Accepted Papers

Conditionally accepted papers will be added once their acceptance is confirmed.

Research Papers

• A Multi-Width Parametric Equivalence Solver
  Luigi Rinaldi (University College London); John Wickerson (Imperial College London); Samuel Coward (University College London)

• A Practical Specification Language for Automatic Quantum Program Verification
  Wei-Lun Tsai (National Taiwan University); Yu-Fang Chen (Academia Sinica); Ondřej Lengál (Brno University of Technology)

• A mechanised, bidirectional type system for bit-width determination in SystemVerilog
  Gabriel Desfrene (École normale supérieure – PSL); Quentin Corradi, Michalis Pardalos, John Wickerson (Imperial College London)

• A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
  Xiaofeng Zhou, Guangyu Hu (Hong Kong University of Science and Technology); Hongce Zhang (Hong Kong University of Science and Technology (Guangzhou)); Wei Zhang (Hong Kong University of Science and Technology)

• ATKVerifier: Adaptive Top-K Constraints for Tighter Verification of Semantic Segmentation Networks
  Yuehao Liu, Cong Tian (ICTT and ISN Laboratory, Xidian University); Yansong Dong (Beijing Sunwise Information Technology Ltd); Liang Zhao, Chao Huang, Wensheng Wang (ICTT and ISN Laboratory, Xidian University)

• An L# Based Algorithm for Active Learning of Minimal Separating Automata
  Jasper Laumen, Leonne Snel, Frits Vaandrager (Radboud University)

• Automated Amortised Analysis of Skew Heaps and Leftist Heaps
  Armin Walch, Georg Moser (University of Innsbruck); Berry Schoenmakers (TU Eindhoven, Netherlands); Florian Zuleger (Vienna University of Technology)

• Automating Bitvector and Finite Field Equivalence Proofs in Lean
  Elizaveta Pertseva (Stanford University); Valentin Robert (Galois, Inc.); Clark Barrett (Stanford University); James Parker (Galois, Inc.)

• Best-Effort Safety Control of Multi-Mode Systems
  Massimo Benerecetti, Marco Faella, Fabio Mogavero (University of Naples, Italy)

• Complete Local Reasoning About Parameterized Programs Over Topologies
  Ruotong Cheng, Azadeh Farzan (University of Toronto)

• Compositional Verification of Timed Automata via Violation Assumptions
  Mehran Moeini Jam (TU Wien, Austria; Sharif University of Technology, Iran); Hamed Kalantari (Sharif University of Technology, Iran); Ehsan Khamespanah (University of Tehran, Iran); Marjan Sirjani (Malardalen University, Sweden); Ali Movaghar (Sharif University of Technology, Iran)

• Consistency-Based Software Diagnosis: Accuracy, Scalability, and Limitations
  Sarah Sallinger, Lukas Graussam, Georg Weissenbacher, Florian Zuleger (TU Wien); Alexey Ignatiev (Monash University)

• Deadlock Verification via Ordering-Constrained Mutex Modeling
  Pei Wang, Zhilei Han, Zhihang Sun, Fei He (Tsinghua University)

• Decoupled Planning for Multiple Omega-Regular Objectives
  Guy Avni (University of Haifa, Israel); Thomas A. Henzinger (Institute of Science and Technology, Austria); Kaushik Mallik (IMDEA Software Institute, Spain); Suman Sadhukhan (TU Clausthal, Germany); K.S. Thejaswini (Institute of Science and Technology, Austria)

• Differentially Private Runtime Monitoring
  Frederik Scheerer, Bernd Finkbeiner (CISPA Helmholtz Center for Information Security)

• Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
  Milan Ceska (Brno University of Technology); Sebastian Junges, Luko van der Maas (Radboud University); Filip Macák (Brno University of Technology); Tim Quatmann (RWTH Aachen University)

• Formal Verification of Quantum Ancilla Safety
  Jiqi Li (Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software Chinese Academy of Sciences, University of Chinese Academy of Sciences); Jingyi Mei (Leiden University); Wang Fang (University of Edinburgh); Ji Guan (Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software Chinese Academy of Sciences)

• Formally Verified Linear-Time Invertible Lexing
  Samuel Chassot, Viktor Kunčak (EPFL)

• How Many Circuit Identities Are Needed to Generate All Others?
  Yuantian Ding (Purdue University); Nengkun Yu (Stony Brook University); Xiaokang Qiu (Purdue University)

• HyperLasso: Bounded Model Checking of ∀+∃+-Liveness Hyperproperties
  Alcino Cunha, Hugo Pacheco, Nuno Macedo (Universidade do Minho & INESC TEC)

• Improving Stability of SMT Solvers via Context-Driven Normalization
  Xiang Zhang, Mengyu Zhao, Shaohuang Chen, Jian Zhang (Institute of Software, Chinese Academy of Sciences); Shaowei Cai (Beihang University; Institute of Software, Chinese Academy of Sciences)

• Incremental Inference for Probabilistic Datalog
  Xuyang Li, Weiyi Chen (Purdue University); Isil Dillig (UT Austin); Jingbo Wang (Purdue University)

• Lagrangian-Based Duality for Quantified SMT Algorithms
  Ivana Bocevska (TU Wien); Takeshi Tsukada (Chiba University); Hiroshi Unno (Tohoku University); Oded Padon (Weizmann Institute of Science); Sharon Shoham (Tel Aviv University)

• Liquid Tree Automata
  Ashish Mishra (Indian Institute of Technology Hyderabad); Suresh Jagannathan (Purdue University)

• Liveness Proofs for Hardware Model Checking
  Nils Froleyks (KU Leuven); Emily Yu (Leiden University); Bart Bogaerts (KU Leuven); Armin Biere (University of Freiburg); Keijo Heljanko (University of Helsinki)

• Massively Parallel Mining of Specifications for Hardware Designs
  Leiqi Ye, Guy Frankel, Jianyi Cheng, Elizabeth Polgreen (University of Edinburgh)

• Model Checking Matrix Product States Against Linear Chain Logic
  Ming Xu, Yihao Chen (East China Normal University); Ji Guan (Chinese Academy of Sciences)

• Modular Reasoning about Object Relations
  Micha Greutmann, Marco Eilers, Peter Müller (ETH Zürich)

• On the Complexity of Checking Soundness of Natural Reductions
  Constantin Enea (LIX - CNRS - Ecole Polytechnique); Azadeh Farzan (University of Toronto); Dominik Klumpp (LIX - CNRS - Ecole Polytechnique)

• On the Verification Problem of Remote Direct Memory Access Programs
  Parosh Aziz Abdulla, Mohamed Faouzi Atig (Uppsala University); R Govind (The Institute of Mathematical Sciences, Chennai); Stephan Spengler (Uppsala University)

• Over-approximation of weakly-hard constraints for control systems verification
  Rieke de Maeyer, Holger Hermanns, Martina Maggio (Saarland University)

• Parallel Abstract Interpretation for Polynomial Programs with Range Bound Assertions
  S. Akshay (Indian Institute of Technology Bombay); Supratik Chakraborty (IIT Bombay); Soroush Farokhnia (HKUST); Amir Goharshady (University of Oxford); Harshit Jitendra Motwani (TU Wien); Đorđe Žikelić (Singapore Management University)

• Perception with Guarantees: Certified Pose Estimation via Reachability Analysis
  Tobias Ladner (Technical University of Munich); Yasser Shoukry (University of California, Irvine); Matthias Althoff (Technical University of Munich)

• Polynomial Invariant Generation for Floating Point Programs
  Xuran Cai (University of Oxford); Liqian Chen (National University of Defense Technology); Hongfei Fu (Shanghai Jiao Tong University)

• Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement
  Hengjie Liu, Zhenya Zhang, Jianjun Zhao (Kyushu University)

• Quantifying Sensitivity for Tree Ensembles : A symbolic and compositional approach
  Ajinkya Naik, Akshay S, Ashutosh Gupta, Chaitanya Garg (IIT Bombay); Kuldeep S. Meel (University of Toronto)

• Randomise Alone, Reach Together
  Léonard Brice, Thomas A. Henzinger, Alipasha Montaseri, Ali Shafiee, K. S. Thejaswini (Institute of Science and Technology Austria)

• SMT-Based Active Learning of Weighted Automata
  Tiago Ferreira (University College London); Kevin Batz, Alexandra Silva (Cornell University)

• Satisfiability Modulo Extensional Constant Arrays
  Mathias Preiner, Aina Niemetz, Clark Barrett (Stanford University)

• Scalable Deductive Verification of Data-Level Parallel Programs
  Lars van den Haak (Eindhoven University of Technology); Marieke Huisman (University of Twente); Anton Wijs (Eindhoven University of Technology)

• Shields to Guarantee Probabilistic Safety in MDPs
  Linus Heck (Radboud University); Filip Macák, Roman Andriushchenko, Milan Ceska (Brno University of Technology); Sebastian Junges (Radboud University)

• Sound and Precise Symbolic Automata Model for Stateful Software Systems
  Xinlong Wu, Ruiyu Zhou (Nanjing University); Peisen Yao (Zhejiang University); Qingkai Shi (Nanjing University)

• Spatiotemporal Robustness of Temporal Logic Tasks using Multi-Objective Reasoning
  Oliver Schön, Lars Lindemann (ETH Zürich)

• String Solving with Stabilization and Transducers
  David Chocholatý, Vojtěch Havlena, Juraj Síč (Brno University of Technology); Lukáš Holík, Michal Šedý (Aalborg University)

• Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning
  Debraj Chakraborty (Nanyang Technological University); Anirban Majumdar (Tata Institute of Fundamental Research); Prince Mathew (Université Libre de Bruxelles); Sayan Mukherjee (Univ Rennes, Inria, CNRS, IRISA); Jean-François Raskin (Université Libre de Bruxelles)

• Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains
  Jianlin Li, Nick Guo, Peter Ye, Yizhou Zhang (University of Waterloo)

• The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver
  Andrew Reynolds, Hans-Jörg Schurr (The University of Iowa); Haniel Barbosa (Universidade Federal de Minas Gerais); Abdalrhman Mohamed, Hanna Lachnitt, Jibiana Zoe Jakpor (Stanford University); Yoni Zohar, Ofec Israel (Bar Ilan University); Clark Barrett (Stanford University); Cesare Tinelli (The University of Iowa); Aina Niemetz, Mathias Preiner (Stanford University)

• The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq
  Andrei Aleksandrov (Fraunhofer Institute FOKUS Berlin); Malte Jackisch, Kim Völlinger (Technische Universität Berlin)

• Transition Invariants Revisited: Termination Witnesses and Their Validation
  Dirk Beyer, Marek Jankola, Marian Lingsch-Rosenfeld (LMU Munich)

• Upper Bound for the Determinization of Emerson-Lei Automata: A One-Fin Approach
  Runzhe Ma, Cong Tian, Wensheng Wang, Zhenhua Duan (ICTT and ISN Laboratory, Xidian University)

• VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification
  Ann Roy, Allen Antony (University of Western Australia); Andrea Gimelli (University of Genova); Matthew Daggitt (University of Western Australia)

• Weighted soundness for Workflow Nets
  Filip Mazowiecki, Piotr Hofman, Krzysztof Makuracki (University of Warsaw)

Tool Papers

• A Tool for the Verification and Synthesis of Stochastic World Models
  Radu Calinescu, Micah Bassett, Brendan Devlin-Hill, Simos Gerasimou, Sinem Getir Yaman, Kavan Fatehi, Gricel Vázquez (University of York)

• Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers
  Joe Hattori, Naoki Kobayashi, Ken Sakayori (The University of Tokyo)

• Automatic heap memory diagrams for separation logic proofs in Rocq
  Yawen Guan, Shardul Chiplunkar, Clément Pit-Claudel (EPFL)

• Burrow: A Proof Framework for Weak Memory
  Dennis Sprokholt (TU Munich); Soham Chakraborty (TU Delft)

• Caesar: A Deductive Verifier for Probabilistic Programs
  Philipp Schröer (RWTH Aachen University); Kevin Batz (Cornell University); Umut Yiğit Dural, Darion Haase (RWTH Aachen University); Benjamin Lucien Kaminski (Saarland University and University College London); Joost-Pieter Katoen (RWTH Aachen University); Christoph Matheja (DTU Compute and University of Oldenburg)

• Extending QuAK with Nested Quantitative Automata
  Thomas A. Henzinger (Institute of Science and Technology Austria); Nicolas Mazzocchi (Slovak University of Technology in Bratislava); N. Ege Saraç (CISPA Helmholtz Center for Information Security); Harun Yılmaz (Sabancı University)

• Fast Obligation Translation and Synthesis
  Alexandre Duret-Lutz (LRE / EPITA); Giuseppe De Giacomo (University of Oxford); Marcin Jurdzinski (DIMAP, University of Warwick); Nir Piterman (University of Gothenburg & Chalmers University of Technology); Moshe Y. Vardi (Rice University); Shufang Zhu (University of Liverpool)

• HyperQB 2.0: A Bounded Model Checker for Hyperproperties
  Tzu-Han Hsu, Milad Rabizadeh, Kenneth Rogale, Fedor Filippov, Marco A. de Oliveira Batista, Borzoo Bonakdarpour (Michigan State University)

• KoAT: Automatic Complexity and Termination Analysis of Integer Programs
  Nils Lommen, Jürgen Giesl, Eleanore Meyer (RWTH Aachen University)

• Kofola 1.0: A Modular Approach to 𝝎-Regular Complementation and Inclusion Checking
  Ondrej Alexaj, Vojtěch Havlena (Brno University of Technology); Lukáš Holík (Brno University of Technology and Aalborg University); Ondřej Lengál (Brno University of Technology); Yong Li (Institute of Software, Chinese Academy of Sciences); Nicolas Mazzocchi (Slovak University of Technology in Bratislava)

• Mallob: Scalable Automated Reasoning On Demand
  Dominik Schreiber, Niccolò Rigi-Luperti, Peter Sanders (Karlsruhe Institute of Technology)

• Octopus: Practical Equivalence Checking of P4 Packet Parsers
  Jort van Leenen, Tobias Kappé (LIACS, Leiden University)

• PSF: A Generic and Extensible Framework for Protocol State Fuzzing
  Konstantinos Sagonas (Uppsala University & National Technical University of Athens); Thanos Typaldos (Yale University & National Technical University of Athens)

• PyCHC: a Framework for Certified Horn Solving and CHC-based Design
  Anna Becchi (University of Lugano); Martin Blicha (Argot Collective); Rodrigo Otoni (University of Groningen); Natasha Sharygina (University of Lugano)

• SemML 2.0: Synthesizing Controllers from LTL
  Maximilian Prokop (TU Munich); Tobias Meggendorfer (Lancaster University Leipzig); Jan Kretinsky (Masaryk University Brno)

• SvLibChecker: A Light-Weight Tool for Software Model Checking
  Dirk Beyer, Marian Lingsch-Rosenfeld (LMU Munich)

• sweap: Reactive Synthesis for Infinite-State Integer Problems
  Shaun Azzopardi (Dedaub); Luca Di Stefano (TU Wien); Nir Piterman (University of Gothenburg, Chalmers University of Technology)

• TACO: A Toolsuite for the Verification of Threshold Automata
  Paul Eichler, Tom Baumeister (CISPA Helmholtz Center for Information Security); Mouhammad Sakr (American University of Beirut); Mahboubeh Kalateh Dowlati, Marcus Völp (Luxembourg University); Swen Jacobs (CISPA Helmholtz Center for Information Security)

• The TLA+ Model Checker Apalache
  Rodrigo Otoni (University of Groningen); Shon Feder (Tarides); Jure Kukovec, Andrey Kupriyanov (Independent Researcher); Gabriela Moreira, Philip Offtermatt (Informal Systems); Thomas Pani, Thanh-Hai Tran, Igor Konnov (Independent Researcher)

• Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean
  Vladimir Gladshtein (National University of Singapore); Vitaly Kurin (Neapolis University Pafos); Yueyang Feng, Dipesh Kafle, George Pîrlea, Qiyuan Zhao, Ilya Sergey (National University of Singapore)

Industrial Experience Reports or Case Studies

• A Neurosymbolic Approach to Natural Language Formalization and Verification
  Chenyang An, Sam Bayless, Stefano Buliani, Darion Cassel (Amazon Web Services); Byron Cook (Amazon Web Services, University College London); Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, Victor Heorhiadi, Marc Hudak, Dejan Jovanović, Andrew M. Kent, Benjamin Kiesl-Reiter, Jeffrey J. Kuna, Nadia Labai, Joseph Lilien, Divya Raghunathan, Zvonimir Rakamarić, Niloofar Razavi, Michael Tautschnig, Ali Torkamani, Nathaniel Weir, Michael W. Whalen (Amazon Web Services); Jianan Yao (University of Toronto)

• Analysis and Verification of Quantum Communication Protocols in UPPAAL
  René Bødker Christensen, Nikolaj Rossander Kristensen, Kim Guldstrand Larsen, Marius Mikučionis, Jiří Srba, Loke Walsted (Aalborg University)

• Ensuring Safety in Automotive Machine Learning Inference: From Pre-validated Static Kernels to Machine Learning Graph Compilation
  Jelena Frtunikj, Alex Latz, Ajit Mistry, Matthew Propp, Vasu Singh, Suresh Talapaneni, Amanda Tang, Damien Zufferey (NVIDIA)

• Model Checking for Flexible Network Protocols
  Andrew Johnson (Princeton University); Dennis Fetterly, Jon Zolla, Sean Song (Google, Inc.)

• Show Me The Money: An Exercise in Proof-Driven Software Understanding
  Joseph Tafese (University of Waterloo); Karthik Nukala (SRI); Hassen Saidi (Entalus); Natarajan Shankar (SRI); Arie Gurfinkel (University of Waterloo); Giuliano Losa (Stellar Development Foundation)

• The Simulator’s Blueprint: Automata Learning from Cybersecurity Logs
  Tudor Braicu, Benjamin Ylvisaker, Nico Espinosa Dice, Yiding Chen, Yiyi Zhang (Cornell University); Nate Foster (EPFL); Hossein Hojjat (Tehran Institute for Advanced Studies, Khatam University)