Programme

• Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer and Brijesh Dongol. Intel PMDK Transactions: Specification and Concurrency
• Léo Stefanesco, Azalea Raad and Viktor Vafeiadis. Specifying and Verifying Persistent Libraries
• Sumanth Prabhu, Grigory Fedyukovich and Deepak D’Souza. Maximal Quantified Precondition Synthesis for Linear Array Loops
• Hrutvik Kanabar, Kacper Korban and Magnus O. Myreen. Verified Inlining and Specialisation for PureCake
• Liye Guo and Cynthia Kop. Higher-Order LCTRSs and Their Termination
• Liang-Ting Chen and Hsiang-Shang Ko. A Formal Treatment of Bidirectional Typing
• Jack Hughes and Dominic Orchard. Program Synthesis from Graded Types
• Jason Z. S. Hu and Brigitte Pientka. Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis
• Sven Keidel, Dominik Helm, Tobias Roth and Mira Mezini. A Modular Soundness Theory for the Blackboard Analysis Architecture
• Cyril Cohen, Enzo Crance and Assia Mahboubi. Trocq: Proof Transfer for Free, With or Without Univalence
• Raphaël Monat, Aymeric Fromherz and Denis Merigoux. Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
• Hiroya Fujinami and Ichiro Hasuo. Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping
• Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni. Monadic Intersection Types, Relationally
• Andrea Colledan and Ugo Dal Lago. Circuit Width Estimation via Effect Typing and Linear Dependency
• Daniel Lundén, Lars Hummelgren, Jan Kudlicka, Oscar Eriksson and David Broman. Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
• Shachar Itzhaky, Sharon Shoham and Yakir Vizel. Hyperproperty Verification as CHC Satisfiability
• Théo Laurent, Meven Lennon-Bertrand and Kenji Maillard. Definitional Functoriality for Dependent (Sub)Types
• Anders Ågren Thuné, Kazutaka Matsuda and Meng Wang. Reconciling Partial and Local Invertibility
• Loïc Pujet and Nicolas Tabareau. Observational Equality Meets CIC
• Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix. On the Hardness of Analyzing Quantum Programs Quantitatively
• Yotam Dvir, Ohad Kammar and Ori Lahav. A Denotational Approach to Release-Acquire Concurrency
• Pierre Lermusiaux and Benoit Montagu. Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation
• Thiago Felicissimo. Generic Bidirectional Typing for Dependent Type Theories
• Sam Lindley, Cristina Matache, Sean Moss, Sam Staton, Nicolas Wu and Zhixuan Yang. Scoped Effects as Parameterized Algebraic Theories
• Elaine Li, Felix Stutz and Thomas Wies. Deciding Subtyping for Asynchronous Multiparty Sessions
• Luis Caires and Bernardo Toninho. The Session Abstract Machine

• Lucas Sakizloglou, Holger Giese and Leen Lambers. Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models
• Margarita Capretto, Martin Ceresa and Cesar Sanchez. Monitoring the Future of Smart Contracts
• Omar Al-Bataineh. Invariant-based Program Repair
• Jan H. Boockmann and Gerald Luettgen. Comprehending Object State via Dynamic Class Invariant Learning
• Yliès Falcone, Gwen Salaün and Ahang Zuo. Probabilistic Runtime Enforcement of Executable BPMN Processes
• Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg and Mariëlle Stoelinga. Fuzzy quantitative attack tree analysis
• Cedric Richter and Heike Wehrheim. Can ChatGPT support software verification?
• Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang and Zhiping Shi. Refinement Verification of OS Services based on a Verified Preemptive Microkernel
• He Xu, Sven Schneider and Holger Giese. Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems
• Téo Bernier, Yani Ziani, Nikolai Kosmatov and Frédéric Loulergue. Combining Deductive Verification with Shape Analysis
• Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho and Ruben Martins. Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation
• Geunyeol Yu, Seunghyun Chae, Kyungmin Bae and Sungkun Moon. Formal Specification of Trusted Execution Environment APIs
• Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang and Guojun Ma. Smart Issue Detection for Large-Scale Online Service Systems Using Multi-Channel Data
• Dré van Oorschot, Marieke Huisman and Ömer Şakar. First Steps towards Deductive Verification of LLVM IR

• Pete Austin, Sougata Bose and Patrick Totzke. Parity Games on Temporal Graphs
• Philip Saville. Clones, Closed Categories, and Combinatory Logic
• Bart Jacobs. Drawing from an Urn is Isometric
• Patrick Baillot, Ugo Dal Lago, Cynthia Kop and Deivid Vale. On Basic Feasible Functionals and the Interpretation Method
• Andrei Draghici, Christoph Haase and Andrew Ryzhikov. Reachability in Fixed VASS: Expressiveness and Lower Bounds
• Daniel Hausmann, Nir Piterman, Irmak Saglam and Anne-Kathrin Schmuck. Fair Omega-regular Games
• Orna Kupferman, Ofer Leshkowitz and Naama Shamash Halevy. Synthesis with Privacy Against an Observer
• Dario Stein and Richard Samuelson. Towards a Compositional Framework for Convex Analysis (with Applications to Probability Theory)
• Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas and Henning Urbat. Logical Predicates in Higher-Order Mathematical Operational Semantics
• Fabian Birkmann, Stefan Milius and Henning Urbat. Monoidal Extended Stone Duality
• Jesse Comer and Balder ten Cate. Craig Interpolation for Decidable First-Order Fragments
• Beniamino Accattoli and Adrienne Lancelot. Light Genericity
• Jan-Christoph Kassing, Florian Frohn and Jürgen Giesl. From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
• Valentin Blot, Gilles Dowek, Thomas Traversié and Théo Winterhalter. From Rewrite Rules to Axioms in the lambdaPi-Calculus Modulo Theory
• Laurent Doyen, Pranshu Gaba and Shibashis Guha. Stochastic Window Mean-payoff Games
• Lucie Guillou, Corto Mascle and Nicolas Waldburger. Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
• Philipp Czerner, Javier Esparza and Valentin Krasotin. A Resolution-Based Interactive Proof System for UNSAT
• Luca Geatti, Alessio Mansutti and Angelo Montanari. Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems
• Alejandro Villoria, Henning Basold and Alfons Laarman. Enriching Diagrams with Algebraic Operations
• Daniel Hausmann, Mathieu Lehaut and Nir Piterman. Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
• Shaull Almagor and Neta Dafni. Determinization of Integral Discounted-Sum Automata is Decidable
• Shaull Almagor, Guy Avni, Henry Sinclair-Banks and Asaf Yeshurun. Dimension-Minimality and Primality of Counter Nets
• Aditya Prakash. Checking History-Determinism is NP-hard for Parity Automata
• Marek Jankola and Jan Strejček. Tighter Construction of Tight Büchi Automata

Regular Research Papers

• Mayank Solanki, Prantik Chatterjee, Akash Lal and Subhajit Roy. Accelerated Bounded Model Checking Using Interpolation Based Summaries
• Satya Prakash Nayak and Anne-Kathrin Schmuck. Most General Winning Secure Equilibria Synthesis in Graph Games
• Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot and Sebastian Junges. Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
• Marijn Heule and Manfred Scheucher. Happy ending: An empty hexagon in every set of 30 points
• Leonardo Lima, Jonathan Huerta Y Munive and Dmitriy Traytel. Explainable Online Monitoring of Metric First-Order Temporal Logic
• Yubo Cai and Gleb Pogudin. Dissipative quadratizations of polynomial ODE systems
• S. Akshay, Eliyahu Basa, Dror Fried and Supratik Chakraborty. On Dependent Variables in Reactive Synthesis
• Lukas Westhofen, Christian Neurohr, Daniel Neider and Jean Christoph Jung. Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains
• Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
• Xiyue Zhang, Benjie Wang and Marta Kwiatkowska. Provable Preimage Under-Approximation for Neural Networks
• Laura Bocchi, Andy King and Maurizio Murgia. Asynchronous Subtyping by Trace Relaxation
• Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas and Fredrik Tåquist. Scalable Tree-based Register Automata Learning
• Nishant Rodrigues, Mircea Sebe, Xiaohong Chen and Grigore Rosu. A Logical Treatment of Finite Automata
• Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán and Yon Shin Teo. A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation
• Abhishek Kr Singh and Ori Lahav. Decidable Verification under Localized Release-Acquire Concurrency
• Antonio Jiménez-Pastor, Kim Guldstrand Larsen, Mirco Tribastone and Max Tschaikowski. Forward and Backward Constrained Bisimulations for Quantum Circuits
• Rüdiger Ehlers and Ayrat Khalimov. Fully Generalized Reactivity(1) Synthesis
• Aditi Kabra, Jonathan Laurent, Stefan Mitsch and André Platzer. CESAR: Control Envelope Synthesis via Angelic Refinements
• Raven Beutner. Automated Software Verification of Hyperliveness
• Martin Jonáš, Jan Strejček, Marek Trtík and Lukáš Urban. Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage
• Muhammad Osama and Anton Wijs. Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
• Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger. Deciding Boolean Separation Logic via Small Models
• Rupak Majumdar, Irmak Saglam and K. S. Thejaswini. Rabin Games and Colourful Universal Trees
• Loes Kruger, Sebastian Junges and Jurriaan Rot. Small Test Suites for Active Automata Learning
• Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr. Learning Explainable and Better Performing Representations of POMDP Strategies
• Mohit Tekriwal, Avi-Tachna Fram, Jean-Baptiste Jeannin, Manos Kapritsos and Dimitra Panagou. Formally verified asymptotic consensus in robust networks
• Anna Blume Jakobsen, Rasmus Skibdahl Melanchton Jorgensen, Andreas Pavlogiannis and Jaco van de Pol. Fast Symbolic Computation of Bottom SCCs
• Guy Avni, Kaushik Mallik and Suman Sadhukhan. Auction-Based Scheduling
• Dong Xu, Nusrat Jahan Mozumder, Hai Duong and Matthew Dwyer. Training for Verification: Increasing Neuron Stability to Scale DNN Verification
• Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike and John Backes. DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
• Florian Furbach, Parosh Aziz Abdulla, Mohamed Faouzi Atig and Shashwat Garg. Verification under TSO with an infinite Data Domain
• Sumanth Prabhu, Deepak D’Souza, Supratik Chakraborty, Venkatesh R and Grigory Fedyukovich. Weakest Precondition Inference for Non-Deterministic Linear Array Programs
• Hari Govind Vediramana Krishnan, Isabel Garcia-Contreras, Sharon Shoham and Arie Gurfinkel. Speculative SAT modulo SAT
• Thibault Hilaire, David Ilcinkas and Jérôme Leroux. A State-of-the-Art Karp-Miller Algorithm Certified in Coq
• Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga and Nils Jansen. CTMCs with Imprecisely Timed Observations

Case Study Papers

• Lukas Koenig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kueperkoch, Dennis Fassbender and Michael Hanselmann. Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
• Leping Zhang, Yongwang Zhao and Jianxin Li. A Comprehensive Specification and Verification of the L4 Microkernel API
• Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler and Sascha Witt. Formally Verifying an Efficient Sorter

Tool Demo Papers

• Md Solimul Chowdhury, Cayden Codel and Marijn Heule. TaSSAT: Transferring and Sharing in SAT
• Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč. Z3-Noodler: An Automata-based String Solver
• Mertcan Temel. VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification
• Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov. Automate where Automation Fails: Proof Strategies for Frama-C/WP

Regular Tool Papers

• Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci and Jaco van de Pol. On-The-Fly Algorithm for Reachability in Parametric Timed Games
• Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee and Nils Sirrenberg. Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers
• Matthias Cosler, Christopher Hahn, Ayham Omar and Frederik Schmitt. NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
• Nils Husung, Clemens Dubslaff, Holger Hermanns and Maximilian Alexander Köhl. OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust
• Michalis Kokologiannakis, Viktor Vafeiadis and Rupak Majumdar. Enhancing GenMC’s Usability and Performance
• David Chocholatý, Tomas Fiedor, Vojtěch Havlena, Lukáš Holík, Martin Hruska, Ondrej Lengal and Juraj Síč. Mata: A Fast and Simple Finite Automata Library
• Tom van Dijk, Feije van Abbema and Naum Tomov. Knor: reactive synthesis using Oink
• Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi. JPF: From 2003 to 2023
• Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo and Dongjie He. SootUp: A Redesign of the Soot Static Analysis Framework
• Lars B. van den Haak, Anton Wijs, Marieke Huisman and Mark van den Brand. HaliVer: Deductive Verification and Scheduling Languages Join Forces
• Hanna Lachnitt, Cesare Tinelli, Andrew Reynolds, Andres Noetzli, Haniel Barbosa, Leni Aniva, Clark Barrett and Mathias Fleury. IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL