Programme

• Jonathan Chan, Stephanie Weirich. Stratified Type Theory
• Roméo La Spina, Sandrine Blazy, Delphine Demange. Formal Verification of WTO-based Dataflow Solvers
• Wenjia Ye, Matías Toro, Claudio Gutierrez, Bruno C. D. S. Oliveira, Éric Tanter. Elucidating Type Conversions in SQL Engines
• Beniamino Accattoli. The Vanilla Sequent Calculus is Call-by-Value
• Risa Yamada, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato. On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic
• Felix Stutz, Emanuele D’Osualdo. An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
• Rongen Lin, Hongjin Liang, Xinyu Feng. Verifying Algorithmic Versions of the Lovász Local Lemma
• Weijie Fan, Hongjin Liang, Xinyu Feng, Hanru Jiang. A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model
• Joseph Eremondi, Ohad Kammar. Coverage Semantics for Dependent Pattern Matching
• Giovanni Bernardi, Ilaria Castellani, Paul Laforgue, Léo Stefanesco. Constructive characterisations of the must-preorder for asynchrony
• Lucas Cordeiro, Matthew Daggitt, Julien Girard-Satabin, Omri Isac, Taylor T. Johnson, Guy Katz, Ekaterina Komendantskaya, Augustin Lemesle, Edoardo Manino, Artjoms Šinkarovs, Haoze Wu. Neural Network Verification is a Programming Language Challenge
• Guillaume Ambal, Ori Lahav, Azalea Raad. Sufficient Conditions for Robustness of RDMA Programs
• Yaozhu Sun, Bruno C. d. S. Oliveira. Named Arguments as Intersections, Optional Arguments as Unions
• Thomas EHRHARD, Claudia FAGGIAN, Michele PAGANI. Variable Elimination as Rewriting in a Linear Lambda Calculus
• Marco Giunti, Nobuko Yoshida. Iso-Recursive Multiparty Sessions and their Automated Verification
• Florian Sextl, Adam Rogalewicz, Tomáš Vojnar, Florian Zuleger. Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration
• Amir Kafshdar Goharshady, S Hitarth, Sergei Novozhilov. Efficient Synthesis of Tight Polynomial Upper-bounds for Systems of Conditional Polynomial Recurrences
• Kimball Germane, Tim Whiting. Context-Sensitive Demand-Driven Control-Flow Analysis
• Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, Fabio Zanasi. A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming
• Dragana Milovancevic, Mario Bucev, Marcin Wojnarowski, Samuel Chassot, VIktor Kuncak. Formal Autograding in a Classroom
• Jérôme Boillot, Jérôme Feret. Abstraction of memory block manipulations by symbolic loop folding
• Christian Skalka, Joe Near. SMT-Boosted Security Types for Low-Level MPC
• Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski. An abstract, certified account of operational game semantics
• Sung-Shik Jongmans. First-Person Choreographic Programming with Continuation-Passing Communications
• Matthew Alan Le Brun, Simon Fowler, Ornela Dardha. Multiparty Session Types with a Bang!
• Joseph Bond, Cristina David, Minh Nguyen, Dominic Orchard, Roly Perera. Conjugate Operators for Transparent, Explorable Research Outputs
• Matteo Acclavio, Giulia Manara, Fabrizio Montesi. Formulas as Processes, Deadlock-Freedom as Choreographies
• Pierre Goutagny, Aymeric Fromherz, Raphaël Monat. CUTECat: Concolic Execution for Computational Law
• Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal. Context-Dependent Effects in Guarded Interaction Trees
• Andrei Paskevich, Paul Patault, Jean-Christophe Filliâtre. Coma, an Intermediate Verification Language with Explicit Abstraction Barriers

• Matt Earnshaw and Mario Román. Context-Free Languages of String Diagrams
• Linan Chen, Florence Clerc and Prakash Panangaden. A behavioural pseudometric for continuous-time Markov processes
• Daniel Gratzer, Mathias Adam Møller and Lars Birkedal. Idempotent Resources in Separation Logic
• Marco Bernardo, Andrea Esposito and Claudio Antares Mezzina. Alternative Characterizations of Hereditary History-Preserving Bisimilarity via Backward Ready Multisets
• Vojtěch Havlena, Ondrej Lengal and Barbora Šmahlíková. Complementation of Emerson-Lei Automata
• Pedro Nora, Jurriaan Rot, Lutz Schröder and Paul Wild. Relational Connectors and Heterogeneous Simulations
• Esaïe Bauer and Alexis Saurin. On the cut-elimination of the modal $\mu$-calculus: Linear Logic to the rescue
• Kinnari Dave, Louis Lemonnier, Romain Péchoux and Vladimir Zamdzhiev. Combining quantum and classical control: syntax, semantics and adequacy
• Kevin Batz, Joost-Pieter Katoen and Nora Orhan. Quantifier Elimination and Craig Interpolation: The Quantitative Way
• Bálint Kocsis and Jurriaan Rot. Complete Test Suites for Automata in Monoidal Closed Categories
• Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty and César Sánchez. Temporal Hyperproperties for Population Protocols
• Leandro Gomes, Patrick Baillot and Marco Gaboardi. BiGKAT: an algebraic framework for relational verification of probabilistic programs
• Tobias Kappé and Todd Schmid. A General Completeness Theorem for Skip-free Star Algebras
• Pablo Barenbaum and Eduardo Bonelli. Sharing and Linear Logic with Restricted Access
• Filippo Bonchi, Alessandro Di Giorgio and Elena Di Lavore. A Diagrammatic Algebra for Program Logics
• Ashwani Anand, Satya Prakash Nayak, Ritam Raha, Irmak Saglam and Anne-Kathrin Schmuck. Fair Quantitative Games
• Petr Jancar, Jérôme Leroux and Jiri Valusek. Structural Liveness of Conservative Petri Nets
• Yotam Dvir, Ohad Kammar, Ori Lahav and Gordon Plotkin. Two-sorted algebraic decompositions of Brookes’s shared-state denotational semantics
• Patricia Bouyer, B Srivathsan and Vaishnavi Vishwanath. Model-checking real-time systems: revisiting the alternating automaton route

Regular Research Papers

• Anna Stramaglia, Jeroen J. A. Keiren, Maurice Laveaux and Tim A. C. Willemse. Efficient Evidence Generation for Modal μ-Calculus Model Checking
• Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak and Anne-Kathrin Schmuck. Synthesis of Universal Safety Controllers
• Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger and Patrick Wienhöft. Sound Statistical Model Checking for Probabilities and Expected Rewards
• Chenxi Ji, Huan Zhang and Sayan Mitra. Reachability for Nonsmooth Systems with Lexicographic Jacobians
• Christoph Jabs, Jeremias Berg, Bart Bogaerts and Matti Järvisalo. Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
• Daimy Van Caudenberg, Bart Bogaerts and Leandro Vendramin. Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation
• Daniela Kaufmann and Jérémy Berthomieu. Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs
• Derek Egolf and Stavros Tripakis. Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
• Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný and Đorđe Žikelić. Refuting Equivalence in Probabilistic Programs with Conditioning
• Krishnendu Chatterjee, Mahdi Jafariraviz, Raimundo Saona Urmeneta and Jakub Svoboda. Value Iteration with Guessing for Markov Chains and Markov Decision Processes
• Levente Bajczi, Csanád Telbisz, Dániel Szekeres and András Vörös. On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study)
• Lydia Kondylidou, Andrew Reynolds and Jasmin Blanchette. Augmenting Model-Based Instantiation with Fast Enumeration
• Michael Blondin, Michaël Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza and Jakob Schulz. Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
• Michaël Cadilhac, Antonio Casares and Pierre Ohlmann. Fast value iteration: A uniform approach to efficient algorithms for energy games
• Muhammad Osama, Dimitrios Thanos and Alfons Laarman. Parallel Equivalence Checking of Stabilizer Quantum Circuits on GPUs
• Nicolaj Østerby Jensen, Jiri Srba and Kim Guldstrand Larsen. Token Elimination in Model Checking of Petri Nets
• Orna Kupferman and Ofer Leshkowitz. Synthesis with Guided Environments
• Prince Mathew, Vincent Penelle and A V Sreejith. Learning real-time one-counter automata using polynomially many queries
• Raz Lotan and Sharon Shoham. Implicit Rankings for Verifying Liveness Properties in First-Order Logic
• Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofroň and Natasha Sharygina. Unsatisfiability Proofs for Horn Solving
• Roy Yatskan, Ilia Shevrin and Shahar Maoz. Performance Heuristics for GR(1) Realizability Checking and Related Analyses
• Samuel Teuber, Philipp Kern, Marvin Janzen and Bernhard Beckert. Revisiting Differential Verification: Equivalence Verification with Confidence
• Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken and Krishnendu Chatterjee. Fixed Point Certificates for Reachability and Expected Rewards in MDPs
• Wenhua Li, Quang Loc Le, Yahui Song and Wei-Ngan Chin. Inferring Incorrectness Specifications for Object-Oriented Programs
• Yannik Schnitzer, Alessandro Abate and David Parker. Certifiably Robust Policies for Uncertain Parametric Environments
• Yoav Feisntein, Orna Kupferman and Noam Shenwald. Non-Zero-Sum Games with Multiple Weighted Objectives
• Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh and Huan Zhang. Neural Network Verification with Branch-and-Bound for General Nonlinearities
• Zili Wang, Katherine Kosaian and Kristin Yvonne Rozier. Formally Verifying a Transformation from MLTL Formulas to Regular Expressions

Case Study Papers

• Jan Baumeister, Bernd Finkbeiner, Frederik Scheerer, Julian Siber and Tobias Wagenpfeil. Stream-based Monitoring of Algorithmic Fairness
• Rafael Gonçalves, Filipe Gouveia, Inês Lynce and José Fragoso Santos. Proxy Attribute Discovery in Machine Learning Datasets via Inductive Logic Programming
• Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu and David Basin. Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions

Tool Demo Papers

• Jan Heemstra and Anton Wijs. GPUexplore-prob: Markov Chain State Space Construction and Verification with GPUs
• Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi and N. Ege Saraç. Automating the Analysis of Quantitative Automata with QuAK
• Shufang Zhu and Marco Favorito. LydiaSyft: A Compositional Symbolic Synthesis Framework for LTLf Specifications
• Tian-Fu Chen and Jie-Hong Roland Jiang. SliQSim: A Quantum Circuit Simulator and Property Checker

Regular Tool Papers

• David Chocholatý, Vojtěch Havlena, Lukáš Holík, Jan Hranička, Ondrej Lengal and Juraj Síč. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation
• Jan Kretinsky, Tobias Meggendorfer, Maximilian Prokop and Ashkan Zarkhah. SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
• Jonas Schöpf and Aart Middeldorp. Automated Analysis of Logically Constrained Rewrite Systems using crest
• Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett and Sanmi Koyejo. Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
• Liron Cohen, Reuben Rowe and Matan Shaked. Cyclone: A Heterogeneous Tool for Verifying Infinite Descent
• Mark S. Baranowski, Zvonimir Rakamaric and Ganesh Gopalakrishnan. Equivalence Checking of a libm Port
• Mazigh Saoudi, Souheib Baarir, Julien Sopena and Thibault Lejemble. D-Painless: A Framework for Distributed Portfolio SAT Solving
• Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym and Jan Midtgaard. Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM
• Sung-Shik Jongmans. Multiparty Session Typing, Embedded
• Yakir Vizel and Basel Khouri. Revisiting DRUP-based Interpolants with CaDiCaL 2.0
• Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondrej Lengal, Jyun-Ao Lin and Wei-Lun Tsai. AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs