Accepted Papers


  • Split Gröbner Bases for Satisfiability Modulo Finite Fields
    Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett and Işil Dillig
  • SMT-based Symbolic Model-Checking for Operator Precedence Languages
    Michele Chiari, Luca Geatti, Nicola Gigante and Matteo Pradella
  • Proactive Real-Time First-Order Enforcement
    François Hublet, Leonardo Lima, David Basin, Srdjan Krstic and Dmitriy Traytel
  • Information Flow guided Synthesis with Unbounded Communication
    Bernd Finkbeiner, Niklas Metzger and Yoram Moses
  • Relational Synthesis of Recursive Programs via Constrained Tree Automata
    Anders Miltner, Ziteng Wang, Swarat Chaudhuri and Isil Dillig
  • Simulating Quantum Circuits by Model Counting
    Jingyi Mei, Marcello Bonsangue and Alfons Laarman
  • Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
    Eden Frenkel, Tej Chajed, Oded Padon and Sharon Shoham
  • Boosting Few-Pixel Robustness Verification via Covering Verification Designs
    Yuval Shapira, Naor Wiesel, Shahar Shabelman and Dana Drachsler-Cohen
  • Verifying Global Two-Safety Properties in Neural Networks with Confidence
    Anagha Athavale, Ezio Bartocci, Maria Christakis, Matteo Maffei, Dejan Nickovic and Georg Weissenbacher
  • Toward Liveness Proofs at Scale
    Kenneth McMillan
  • End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
    Shenghao Yuan, Frédéric Besson and Jean-Pierre Talpin
  • Synthesis of Temporal Causality
    Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger and Julian Siber
  • Dynamic Programming for Symbolic Boolean Realizability and Synthesis
    Yi Lin, Moshe Vardi and Lucas Martinelli Tabajara
  • Measurement-based Verification of Quantum Markov Chains
    Ji Guan, Yuan Feng, Andrea Turrini and Mingsheng Ying
  • Verification Algorithms for Automated Separation Logic Verifiers
    Marco Eilers, Malte Schwerhoff and Peter Müller
  • Lexicographic Ranking Supermartingales with Lazy Lower Bounds
    Toru Takisaka, Libo Zhang, Changjiang Wang and Jiamou Liu
  • Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
    Charlie Murphy and Zachary Kincaid
  • Strided Difference Bound Matrices
    Arjun Pitchanathan, Albert Cohen, Oleksandr Zinenko and Tobias Grosser
  • General Anticipatory Runtime Verification
    Raik Hipler, Hannes Kallwies, Martin Leucker and César Sánchez
  • Certified Robust Accuracy of Neural Networks Are Bounded due to Bayes Errors
    Ruihan Zhang and Jun Sun
  • Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
    Florian Lercher and Matthias Althoff
  • Localized Attractor Computations for Infinite-State Games
    Philippe Heim, Satya Prakash Nayak, Rayna Dimitrova and Anne-Kathrin Schmuck
  • The Top-Down Solver Verified: Building Confidence in Static Analyzers
    Yannick Stade, Sarah Tilscher and Helmut Seidl
  • Bisimulation Learning
    Alessandro Abate, Mirco Giacobbe and Yannik Schnitzer
  • Regular Reinforcement Learning
    Taylor Dohmen, Mateo Perez, Fabio Somenzi and Ashutosh Trivedi
  • Collective Contracts for Message-Passing Parallel Programs
    Ziqing Luo and Stephen F. Siegel
  • Distributed SMT Solving Based on Dynamic Variable-level Partitioning
    Mengyu Zhao, Shaowei Cai and Yuhang Qian
  • LTL learning on GPUs
    Mojtaba Valizadeh, Nathanael Fijalkow and Martin Berger
  • Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
    Peter Habermehl, Vojtěch Havlena, Michal Hečko, Lukáš Holík and Ondrej Lengal
  • Compositional Value Iteration with Pareto Caching
    Kazuki Watanabe, Marck van der Vegt, Sebastian Junges and Ichiro Hasuo
  • Formally Certified Approximate Model Counting
    Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen and Kuldeep S. Meel
  • Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
    Shaowei Zhu and Zachary Kincaid
  • What should be observed for optimal reward in POMDPs?
    Alyzia-Maria Konsta, Alberto Lluch Lafuente and Christoph Matheja
  • Verifying Cake Cutting, Faster
    Noah Bertram, Tean Lai and Justin Hsu
  • Probabilistic Access Policies with Automated Reasoning Support
    Shaowei Zhu and Yunbo Zhang
  • Syntax-Guided Automated Program Repair For Hyperproperties
    Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour and Bernd Finkbeiner
  • Avoiding the Shoals – A New Approach to Liveness Checking
    Yechuan Xia, Alessandro Cimatti, Alberto Griggio and Jianwen Li
  • Approximate Relational Reasoning for Quantum Programs
    Peng Yan, Hanru Jiang and Nengkun Yu
  • From Clauses to Klauses
    Joseph Reeves, Marijn Heule and Randal Bryant
  • Predictive Monitoring with Strong Trace Prefixes
    Zhendong Ang and Umang Mathur
  • Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
    Dapeng Zhi, Peixin Wang, Si Liu, Luke Ong and Min Zhang
  • On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
    Chenglin Wang and Fangzhen Lin
  • Parsimonious Optimal Dynamic Partial Order Reduction
    Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson and Konstantinos Sagonas
  • Optimization-Based Model Checking for Complex STL Specifications
    Sota Sato, Jie An, Zhenya Zhang and Ichiro Hasuo
  • Guiding Enumerative Program Synthesis with Large Language Models
    Yixuan Li, Julian Parsert and Elizabeth Polgreen
  • Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
    Jiawan Wang, Wenxia Liu, Muzimiao Zhang, Jiaqi Wei, Yuhui Shi, Lei Bu and Xuandong Li
  • Scalable Bit-Blasting with Abstractions
    Aina Niemetz, Mathias Preiner and Yoni Zohar
  • Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
    Yuning Wang and He Zhu
  • Stochastic Omega-Regular Verification and Control with Supermartingales
    Alessandro Abate, Mirco Giacobbe and Diptarko Roy
  • Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
    Dejin Ren, Zhen Liang, Chenyu Wu, Jianqiang Ding, Taoran Wu and Bai Xue
  • Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
    Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung and Cong Tian


  • A Framework for Debugging Automated Program Verification Proofs via Proof Actions
    Chanhee Cho, Yi Zhou, Jay Bosamiya and Bryan Parno
  • The VerCors Verifier: a Progress Report
    Lukas Armborst, Pieter Bos, Lars van den Haak, Marieke Huisman, Robert Rubbens, Ömer Sakar and Philip Tasche
  • Symbolic Model-Checking Intermediate-Language Tool Suite
    Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi and Kristin Yvonne Rozier
  • Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
    Tobias Meggendorfer and Maximilian Weininger
  • CaDiCaL 2.0
    Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks and Florian Pollitt
  • Interactive Theorem Proving modulo Fuzzing
    Sujit Muduli, Rohan Padulkar and Subhajit Roy
  • soid: A Tool for Legal Accountability for Automated Decision Making
    Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott Shapiro and Ruzica Piskac
  • SMLP: Symbolic Machine Learning Prover
    Franz Brauße, Zurab Khasidashvili and Konstantin Korovin
  • Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
    Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz and Clark Barrett
  • The SemGuS Toolkit
    Keith J.C. Johnson, Andrew Reynolds, Thomas Reps and Loris D’Antoni
  • hevm, a Fast Symbolic Execution Framework for EVM Bytecode
    Dxo, Mate Soos, Zoe Paraskevopoulou, Martin Lundfall and Mikael Brockman
  • Monitizer: Automating Design and Evaluation of Neural Network Monitors
    Stefanie Mohr, Muqsit Azeem, Jan Kretinsky, Sudeep Kanav, Sabine Rieder and Marta Grobelna
  • Arithmetic Solving in Z3
    Nikolaj Bjørner and Lev Nachmanson
  • SolTG: A CHC-based Solidity Test Case Generator
    Konstantin Britikov, Ilia Zlatkin, Grigory Fedyukovich, Leonardo Alt and Natasha Sharygina
  • QReach: A Reachability Analysis Tool for Quantum Markov Chains
    Aochu Dai and Mingsheng Ying
  • mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
    James R. Wilcox, Yotam M. Y. Feldman, Oded Padon and Sharon Shoham


  • Testing the migration from analogical to software-based Railway Interlocking Systems
    Anna Becchi, Alessandro Cimatti and Giuseppe Scaglione
  • Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
    Jan Baumeister, Bernd Finkbeiner, Florian Kohn, Sebastian Schirmer, Christoph Torens, Florian Löhr and Guido Manfredi