Accepted Papers

Research Papers

• Verifying Tree-Manipulating Programs via CHCs
  Marco Faella (University of Naples Federico II); Gennaro Parlato (University of Molise)

• Automatic Verification of Floating-Point Accumulation Networks
  David K. Zhang, Alex Aiken (Stanford University)

• Relational Hoare Logic for Realistically Modelled Machine Code
  Denis Mazzucato (Carnegie Mellon University); Abdalrhman Mohamed (Stanford University); Juneyoung Lee (Amazon Web Services); Clark Barrett (Stanford University); Jim Grundy, John Harrison (Amazon Web Services); Corina Pasareanu (NASA Ames and Carnegie Mellon University)

• Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks
  Marius Bozga, Radu Iosif (Univ. Grenoble Alpes, Grenoble INP, VERIMAG); Arnaud Sangnier (DIBRIS, Univ. of Genova, Italy); Neven Villani (Univ. Grenoble Alpes, Grenoble INP, VERIMAG)

• Automated Verification of Monotonic Data Structure Traversals in C
  Matthew Sotoudeh (Stanford University)

• Verifying Fault-Tolerance of Quantum Error Correction Codes
  Kean Chen, Yuhao Liu (University of Pennsylvania); Wang Fang (University of Edinburgh); Jennifer Paykin, Xin-Chuan Wu, Albert Schmitz (Intel Corporation); Steve Zdancewic, Gushu Li (University of Pennsylvania)

• Full LTL Synthesis over Infinite-state Arenas
  Shaun Azzopardi (N/A); Luca Di Stefano (TU Wien); Nir Piterman, Gerardo Schneider (University of Gothenburg and Chalmers University of Technology)

• Integer Reasoning Modulo Different Constants in SMT
  Elizaveta Pertseva, Alex Ozdemir (Stanford); Shankara Pailoor, Alp Bassa (Veridise); Sorawee Porncharoenwase (Amazon); Işil Dillig (UT Austin); Clark Barrett (Stanford)

• On the Complexity of Checking Mixed Isolation Levels for SQL Transactions
  Ahmed Bouajjani (IRIF, CNRS, University Paris Cité); Constantin Enea (LIX, École Polytechnique, CNRS and Institut Polytechnique de Paris); Enrique Román-Calvo (IRIF, CNRS, University Paris Cité)

• Approximating Fixpoints of Approximated Functions
  Paolo Baldan (University of Padova); Sebastian Gurke (University of Duisburg-Essen, Germany); Barbara König (University of Duisburg-Essen); Tommaso Padoan (Università di Trieste); Florian Wittbold (University of Duisburg-Essen)

• D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
  Yingte Xu (Max Planck Institute for Security and Privacy); Gilles Barthe (Max Planck Institute for Security and Privacy & IMDEA Software Institute); Li Zhou (Institute of Software, Chinese Academy of Sciences)

• Floating-Point Neural Networks Are Provably Robust Universal Approximators
  Geonho Hwang (GIST); Wonyeol Lee (POSTECH); Yeachan Park (Sejong University); Sejun Park (Korea University); Feras Saad (Carnegie Mellon University)

• Assessing the Quality of Binomial Samplers: A Statistical Distance Framework
  Sourav Chakraborty (Indian Statistical Institute); Kuldeep S. Meel (Georgia Institute of Technology); Uddalok Sarkar (Indian Statistical Institute)

• Counter Example Guided Reactive Synthesis for LTL Modulo Theories
  Andoni Rodriguez (IMDEA Software Institute and Universidad Politecnica de Madrid, Spain); Felipe Gorostiaga, Cesar Sanchez (IMDEA Software Institute)

• Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
  Timm Spork, Christel Baier (Technische Universität Dresden); Joost-Pieter Katoen (RWTH Aachen University); Sascha Klüppelholz (Technische Universität Dresden); Jakob Piribauer (Technische Universität Dresden; Universität Leipzig)

• Automated Verification of Consistency in Zero-Knowledge Proof Circuits
  Jon Stephens (University of Texas at Austin); Shankara Pailoor (Veridise Inc); Isil Dillig (University of Texas at Austin)

• Efficient Probabilistic Model Checking for Relational Reachability
  Lina Gerlach (RWTH Aachen Univsersity); Tobias Winkler, Erika Ábrahám (RWTH Aachen University); Borzoo Bonakdarpour (Michigan State University); Sebastian Junges (Radboud University)

• Robust Probabilistic Bisimilarity for Labelled Markov Chains
  Franck van Breugel (York University); Syyeda Zainab Fatmi, Stefan Kiefer, David Parker (University of Oxford)

• A Formally Verified Robustness Certifier for Neural Networks
  James Tobler (University of Queensland); Hira Taqdees Syeda, Toby Murray (University of Melbourne)

• Regex Decision Procedures in Extended RE#
  Ian Erik Varatalu (Tallinn University of Technology); Margus Veanes (MSR Redmond); Ekaterina Zhuchko, Juhan Ernits (Tallinn University of Technology)

• Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
  Yicheng Qian (Stanford University); Joshua Clune (Carnegie Mellon University); Clark Barrett (Stanford University); Jeremy Avigad (Carnegie Mellon University)

• Accelerating Automated Program Verifiers by Automatic Proof Localization
  Kiran Gopinathan (University of Illinois Urbana-Champaign); Dionysios Spiliopoulos (ETH Zurich); Vikram Goyal (National University of Singapore); Peter Müller, Markus Püschel (ETH Zurich); Ilya Sergey (National University of Singapore)

• Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata
  Yong Li (Institute of Software, Chinese Academy of Sciences); Soumyajit Paul, Sven Schewe, Qiyi Tang (University of Liverpool)

• Deeply Optimizing the SAT Solver for the IC3 Algorithm
  Yuheng Su (University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences); Qiusong Yang (Institute of Software, Chinese Academy of Sciences, Beijing, China); Yiwei Ci (Institute of Software, Chinese Academy of Sciences); Yingcheng Li, Tianjun Bu (University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences); Ziyu Huang (Beijing Forestry University)

• On the Almost-Sure Termination of Probabilistic Counter Programs
  Sergei Novozhilov (Zhejiang University; The Hong Kong University of Science and Technology); Mingqi Yang, Mingshuai Chen, Zhiyang Li, Jianwei Yin (Zhejiang University)

• Polyregular Model Checking
  Aliaume Lopez, Rafał Stefański (University of Warsaw)

• Small Decision Trees for MDPs with Deductive Synthesis
  Roman Andriushchenko, Milan Češka (Brno University of Technology); Sebastian Junges (Radboud University); Filip Macák (Brno University of Technology)

• Property Directed Reachability with Extended Resolution
  Yakir Vizel, Andrew Luka (Technion – Israel Institute of Technology)

• Arithmetizing Shape Analysis
  Sebastian Wolff, Ekanshdeep Gupta (New York University); Zafer Esen (Uppsala University); Hossein Hojjat (TeIAS, Khatam University); Philipp Rümmer (University of Regensburg); Thomas Wies (New York University)

• Automata Learning from Preference and Equivalence Queries
  Eric Hsiung, Joydeep Biswas, Swarat Chaudhuri (University of Texas at Austin)

• Infinite-state Liveness Checking with rlive
  Alessandro Cimatti, Alberto Griggio (Fondazione Bruno Kessler); Christopher Johannsen, Kristin Yvonne Rozier (Iowa State University); Stefano Tonetta (FBK)

• Scaling Up Proactive Enforcement
  François Hublet (ETH Zürich); Leonardo Lima (University of Copenhagen); David Basin, Srdjan Krstic (ETH Zürich); Dmitriy Traytel (University of Copenhagen)

• Data-driven Verification of Procedural Programs with Integer Arrays
  Ahmed Bouajjani (Université Paris Cité); Wael-Amine Boutglay (Université Paris Cité and Mohammed VI Polytechnic University); Peter Habermehl (Université Paris Cité)

• Structural operational semantics for functional and security verification of pipelined processors
  Robert Colvin (University of Queensland); Roger Su (Australian National University)

• Scaling GR(1) Synthesis via a Compositional Framework for LTL Discrete Event Control
  Hernán Gabriel Gagliardi (Universidad de Buenos Aires); Victor Braberman (Universidad de Buenos Aires/CONICET); Sebastian Uchitel (Universidad de Buenos Aires, CONICET, Imperial College London)

• Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
  Thom Badings (University of Oxford); Wietze Koops (Lund University); Sebastian Junges (Radboud University); Nils Jansen (Ruhr-University Bochum)

• A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
  Bram Kohlen (University of Twente); Maximilian Schäffeler (TU Munich); Mohammad Abdulaziz (King's College London); Arnd Hartmanns, Peter Lammich (University of Twente)

• Engineering an Efficient Probabilistic Exact Model Counter
  Mate Soos (University of Toronto); Kuldeep S. Meel (Georgia Institute of Technology and University of Toronto)

• Verified and Optimized Implementation of Orthologic Proof Search
  Simon Guilloud, Clément Pit-Claudel (EPFL)

• Branching Bisimulation Learning
  Alessandro Abate (University of Oxford); Mirco Giacobbe (University of Birmingham); Christian Micheletti (University of Padua); Yannik Schnitzer (University of Oxford)

• Automatic Synthesis of Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications
  Samuel Williams, Jyotirmoy Deshmukh (University of Southern California)

• QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols
  Yun-Rong Luo (University of Michigan, Ann Arbor); Aman Goel (AWS); Karem Sakallah (University of Michigan)

• Raven: An SMT-Based Concurrency Verifier
  Ekanshdeep Gupta, Nisarg Patel, Thomas Wies (New York University)

• Counterexample-Guided Commutativity
  Marcel Ebbinghaus, Dominik Klumpp, Andreas Podelski (University of Freiburg)

• FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams
  Ziyuan Wang (Tsinghua); Bin Cheng (NUS); Longxiang Yuan (Tsinghua); Zhengfeng Ji (Tsinghua and Zhongguancun Lab)

• INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition
  Suguman Bansal (Georgia Institute of Technolgy); Ramneet Singh (Indian Institute of Technology Delhi)

• GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency
  Soham Chakraborty (TU Delft); S. Krishna (IIT Bombay); Andreas Pavlogiannis (Aarhus University); Omkar Tuppe (IIT Bombay)

• Deductive Synthesis of Reinforcement Learning Agents for Infinite Horizon Tasks
  Yuning Wang, He Zhu (Rutgers)

• Quantitative Supermartingale Certificates
  Alessandro Abate (University of Oxford); Mirco Giacobbe, Diptarko Roy (University of Birmingham)

• Compositional Abstraction for Timed Systems with Broadcast Synchronization
  Hanyue Chen (Tongji University); Miaomiao Zhang (Tongji Uniersity); Frits Vaandrager (Radboud University)

• Supermartingale Certificates for Quantitative Omega-regular Verification and Control
  Thomas A. Henzinger (IST Austria); Kaushik Mallik (IMDEA Software Institute); Pouya Sadeghi (University of Tehran); Djordje Zikelic (Singapore Management University)

Tool Papers

• A Misconception-Driven Adaptive Tutor for Linear Temporal Logic
  Siddhartha Prasad (Brown University); Ben Greenman (University of Utah, USA); Tim Nelson, Shriram Krishnamurthi (Brown University)

• Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking
  Zhengyang Lu (University of Waterloo); Po-Chun Chien (LMU Munich); Nian-Ze Lee (National Taiwan University); Arie Gurfinkel (University of Waterloo); Vijay Ganesh (Georgia Institute of Technology)

• NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks
  Hai Duong, ThanhVu (Vu) Nguyen (George Mason University); Matthew B Dwyer (University of Virginia)

• ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks
  Tianhao Wei, Hanjiang Hu (Carnegie Mellon University); Luca Marzari (University of Verona); Kai S. Yun, Peizhi Niu, Xusheng Luo, Changliu Liu (Carnegie Mellon University)

• PyCaliper: Python-embedded Infrastructure for RTL Verification and Specification Synthesis
  Adwait Godbole (University of California, Berkeley); Brian Huffman (Intel Labs); Fangfei Liu (Intel); Carlos V Rozas (Intel Labs); Sanjit A. Seshia (University of California, Berkeley)

• Extending AALpy with Passive Learning: A Generalized State-Merging Approach
  Benjamin von Berg, Bernhard Aichernig (TU Graz)

• The Vampire Diary
  Filip Bartek (Czech Technical University in Prague); Ahmed Bhayat (University of Manchester); Robin Coutelier, Marton Hajdu, Matthias Hetzenberger (TU Wien); Petra Hozzova (Czech Technical University in Prague); Laura Kovacs, Jakob Rath (TU Wien); Michael Rawson (University of Southampton); Giles Reger (The University of Manchester); Martin Suda (Czech Technical University in Prague); Johannes Schoisswohl (TU Wien); Andrei Voronkov (The University of Manchester)

• Fifteen Years of Viper
  Marco Eilers, Malte Schwerhoff (ETH Zurich); Alexander J. Summers (University of British Columbia); Peter Müller (ETH Zurich)

• The rIC3 Hardware Model Checker
  Yuheng Su (University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences); Qiusong Yang, Yiwei Ci (Institute of Software, Chinese Academy of Sciences, Beijing, China); Tianjun Bu (University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences); Ziyu Huang (Beijing Forestry University)

• Issy: A Comprehensive Tool for Specification and Synthesis of Infinite-State Reactive Systems
  Philippe Heim, Rayna Dimitrova (CISPA Helmholtz Center for Information Security)

• Panini: An Efficient and Flexible Knowledge Compiler
  Yong Lai (Jilin Univeristy); Kuldeep S. Meel (Georgia Institute of Technology); Roland H. C. Yap (National University of Singapore)

• An Intermediate Program Representation for Optimizing Stream-Based Languages
  Frederik Scheerer, Jan Baumeister, Bernd Finkbeiner, Arthur Correnson (CISPA Helmholtz Center for Information Security)

• SPROUT: A Verifier for Symbolic Multiparty Protocols
  Elaine Li (New York University); Felix Stutz (University of Luxembourg); Thomas Wies (New York University); Damien Zufferey (NVIDIA)

• Charon: An Analysis Framework for Rust
  Son Ho (Inria, Microsoft Azure Research); Guillaume Boisseau (Inria); Lucas Franceschino (Cryspen); Yoann Prak, Aymeric Fromherz (Inria); Jonathan Protzenko (Microsoft Azure Research)

• POPACheck: a Model Checker for probabilistic Pushdown Automata
  Francesco Pontiggia, Ezio Bartocci, Michele Chiari (TU Wien)

• HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses
  Hongjian Jiang, Anthony W. Lin (RPTU and MPI-SWS); Oliver Markgraf (RPTU); Philipp Rümmer (University of Regensburg); Daniel Stan (LRE, Epita)

• LearnLib: 10 years later
  Markus Frohme (Technische Universität Dortmund); Falk Howar (Technische Universität Dortmund, Fraunhofer ISST); Bernhard Steffen (Technische Universität Dortmund)

• Decision Heuristics in MCSat
  Thomas Hader (TU Wien); Ahmed Irfan, Stephane Graham-Lengrand (SRI International)

• PyEuclid: A Versatile Formal Plane Geometry System in Python
  Zhaoyu Li, Hangrui Bi, Jialiang Sun (University of Toronto); Zenan Li (Nanjing University); Kaiyu Yang (Meta FAIR); Xujie Si (University of Toronto)

• Veil: A Framework for Automated and Interactive Verification of Transition Systems
  George Pîrlea, Vladimir Gladshtein (National University of Singapore); Elad Kinsbruner (Technion); Qiyuan Zhao, Ilya Sergey (National University of Singapore)

• StarV: A Qualitative and Quantitative Verification Tool for Learning-enabled Systems
  Hoang-Dung Tran (University of Nebraska Lincoln); SungWoo Choi (University of Nebraska, Lincoln, School of Computing); Yuntao Li, Qing Liu (University of Nebraska-Lincoln); Hideki Okamoto (Toyota NA R&D); Bardh Hoxha (Toyota Research Institute North America); Georgios Fainekos (Toyota Motor North America)

• StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
  Yusuke Kawamoto (AIST); Kentaro Kobayashi (Tsukuba University & AIST); Kohei Suenaga (Kyoto University)

• Lean-SMT: An SMT tactic for discharging proof goals in Lean
  Abdalrhman Mohamed (Stanford University); Tomaz Mascarenhas (Universidade Federal de Minas Gerais); Harun Khan (Stanford University); Haniel Barbosa (Universidade Federal de Minas Gerais); Andrew Reynolds (The University of Iowa, Amazon Web Services); Yicheng Qian (Stanford University); Cesare Tinelli (The University of Iowa); Clark Barrett (Stanford University)

• Surfer – An Extensible Waveform Viewer
  Frans Skarman (Linköping University); Lucas Klemmer, Daniel Große (Johannes Kepler University); Oscar Gustafsson (Linköping University); Kevin Laeufer (Cornell University)

Industrial Experience Reports or Case Studies

• Introducing Certificates to the Hardware Model Checking Competition
  Nils Froleyks (JKU Linz); Emily Yu (Institute of Science and Technology Austria); Mathias Preiner (Stanford University); Armin Biere (University of Freiburg); Keijo Heljanko (University of Helsinki)

• Automated Parameterized Verification of a Railway Protection System with Dafny
  Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Christian Lidström, Gianluca Redondi (Fondazione Bruno Kessler); Giuseppe Scaglione, Matteo Tessi (RFI); Dylan Trenti (Fondazione Bruno Kessler)

• Verifying PETSc Vector Components Using CIVL
  Venkata Narayana Sarma Dhavala, Stephen F. Siegel (University of Delaware); Jan Hueckelheim, Paul Hovland (Argonne National Laboratory)

• Space Explanations of Neural Network Classification
  Faezeh Labbaf, Tomas Kolarik (University of Lugano (USI)); Martin Blicha (University of Lugano (USI), Ethereum Foundation) Grigory Fedyukovich (Florida State University, University of Lugano (USI)); Michael Wand (SUPSI, IDSIA, Lugano); Natasha Sharygina (University of Lugano (USI))