| Lorenz Leutgeb, Georg Moser and Florian Zuleger | Automated Expected Amortised Cost Analysis of Probabilistic Data Structures | |
| Marco Faella and Gennaro Parlato | Reasoning about Data Trees using CHCs | |
| Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo and Juneyoung Lee | SMT-based Translation Validation for Machine Learning Compiler | |
| Ji Guan, Wang Fang and Mingsheng Ying | Verifying Fairness in Quantum Machine Learning | |
| Long H. Pham and Jun Sun | Verifying Neural Networks Against Backdoor Attacks | |
| Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir and Idan Refaeli | Neural Network Robustness as a Verification Property: A Principled Case Study | |
| Joonwon Choi, Adam Chlipala and Arvind | Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols | |
| Eric Goubault and Sylvie Putot | RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems | |
| Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang and Wanwei Liu | PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation | |
| Shaowei Cai, Bohan Li and Xindi Zhang | Local Search For SMT on Linear Integer Arithmetic | |
| Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard and Henrich Lauko | From Spot 2.0 to Spot 2.10: What’s New? | |
| Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga and Matthias Volk | Sampling-Based Verification of CTMCs with Uncertain Rates | |
| Vojtěch Havlena, Ondrej Lengal and Barbora Šmahlíková | Complementing Büchi Automata with Ranker | |
| Peng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen and Min Zhang | Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning | |
| Kishor Jothimurugan, Suguman Bansal, Osbert Bastani and Rajeev Alur | Specification-Guided Learning of Nash Equilibria with High Social Welfare | |
| Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer and Đorđe Žikelić | Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs | |
| Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga and Kohei Suenaga | Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption | |
| Yong Li, Andrea Turrini, Weizhi Feng, Moshe Vardi and Lijun Zhang | Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition | |
| Yucheng Ji, Hongfei Fu, Bin Fang and Haibo Chen | Affine Loop Invariant Generation via Matrix Algebra | |
| Priyanka Golia, Brendan Juba and Kuldeep S. Meel | A Scalable Shannon Entropy Estimator | |
| Kyveli Doveri, Pierre Ganty and Nicolas Mazzocchi | FORQ-based Language Inclusion Formal Testing | |
| Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler | Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions | |
| Leonardo Alt, Martin Blicha, Antti Hyvärinen and Natasha Sharygina | SolCMC: Solidity Compiler’s Model Checker | |
| Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez and Albert Rubio | Distilling Constraints in Zero-Knowledge Protocols | |
| Joshua M. Cohen, Qinshi Wang and Andrew W. Appel | Verified Erasure Correction in Coq with MathComp and VST | |
| Anna Becchi and Alessandro Cimatti | Abstraction Modulo Stability for Reverse Engineering | |
| Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora and Sanjit A. Seshia | UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis | |
| Aina Niemetz, Mathias Preiner and Clark Barrett | Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers | |
| Michael Blondin, Filip Mazowiecki and Philip Offtermatt | Verifying generalised and structural soundness of workflow nets via relaxations | |
| Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg and Emmanuel Baccelli | End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers | |
| Pablo Castro, Pedro R. D’Argenio, Luciano Putruele and Ramiro Demasi | Playing Against Fair Adversaries in Stochastic Games with Total Rewards | |
| Jingbo Wang, Yannan Li and Chao Wang | Synthesizing Fair Decision Trees via Iterative Constraint Solving | |
| Raven Beutner and Bernd Finkbeiner | Software Verification of Hyperproperties Beyond k-Safety | Distinguished Paper Award |
| Andreas Gittis, Eric Vin and Daniel Fremont | Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation | |
| Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare Tinelli | Even Faster Conflicts and Lazier Reductions for String Solvers | |
| Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller and Alexander J. Summers | Sound Automation of Magic Wands | |
| Sebastian Junges and Matthijs T. J. Spaan | Abstraction-Refinement for Hierarchical Probabilistic Models | |
| Brandon Paulsen and Chao Wang | Example Guided Synthesis of Linear Approximations for Neural Network Verification | |
| Stanley Bak, Sergiy Bogomolov, Brandon Hencey, Niklas Kochdumper, Ethan Lew and Kostiantyn Potomkin | Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement | |
| Andreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger and Johann Schumann | Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET | |
| Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu and Subhajit Roy | Data-Driven Invariant Learning for Probabilistic Programs | Distinguished Paper Award |
| Prantik Chatterjee, Jaydeepsinh Meda, Akash Lal and Subhajit Roy | Proof-guided Underapproximation Widening for Bounded Model Checking | |
| Chaitanya Agarwal, Shibashis Guha, Jan Křetínský and Pazhamalai Muruganandham | PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP | |
| Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga and Ichiro Hasuo | The Lattice-Theoretic Essence of Property Directed Reachability Analysis | |
| Ahmed Bouajjani, Wael-Amine Boutglay and Peter Habermehl | Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes | |
| Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger and Julian Siber | Explaining Hyperproperty Violations | |
| Marc Fischer, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh and Martin Vechev | Shared Certificates for Neural Network Verification | |
| Timo P. Gros, Holger Hermanns, Joerg Hoffmann, Michaela Klauck, Maximilian Alexander Köhl and Verena Wolf | MoGym: Using Formal Models for Training and Verifying Decision-making Agents | |
| Bernd Finkbeiner, Niklas Metzger and Yoram Moses | Information Flow Guided Synthesis | |
| Mateus De Oliveira Oliveira | Synthesis and Analysis of Petri Nets from Causal Specifications | |
| Geunyeol Yu, Jia Lee and Kyungmin Bae | STLmc: Robust STL Model Checking of Hybrid Systems using SMT | |