| 2025 | Multiparty Session Typing, Embedded. | Sung-Shik Jongmans |
| 2025 | Reachability for Nonsmooth Systems with Lexicographic Jacobians. | Chenxi Ji, Huan Zhang, Sayan Mitra |
| 2025 | Token Elimination in Model Checking of Petri Nets. | Nicolaj . Jensen, Kim G. Larsen, Jir Srba |
| 2025 | Certifying Pareto-Optimality in Multi Objective Maximum Satisfiability. | Christoph Jabs, Jeremias Berg, Bart Bogaerts, Matti Jrvisalo |
| 2025 | Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM. | Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym, Jan Midtgaard |
| 2025 | GPUexplore | Jan Heemstra, Anton Wijs |
| 2025 | Proxy Attribute Discovery in Machine Learning Datasets via Inductive Logic Programming. | Rafael Gonalves, Filipe Gouveia, Ins Lynce, Jos Fragoso Santos |
| 2025 | Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions. | Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu, David A. Basin |
| 2025 | Synthesis of Universal Safety Controllers. | Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak, Anne-Kathrin Schmuck |
| 2025 | Non-Zero-Sum Games with Multiple Weighted Objectives. | Yoav Feinstein, Orna Kupferman, Noam Shenwald |
| 2025 | Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction. | Derek Egolf, Stavros Tripakis |
| 2025 | RacerF: Data Race Detection with Frama-C (Competition Contribution). | Toms Dack, Toms Vojnar |
| 2025 | Cyclone: A Heterogeneous Tool for Verifying Infinite Descent. | Liron Cohen, Reuben N. S. Rowe, Matan Shaked |
| 2025 | Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. | David Chocholat, Vojtech Havlena, Luks Holk, Jan Hranicka, Ondrej Lengl, Juraj Sc |
| 2025 | SliQSim: A Quantum Circuit Simulator and Solver for Probability and Statistics Queries. | Tian-Fu Chen, Jie-Hong R. Jiang |
| 2025 | AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs. | Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondrej Lengl, Jyun-Ao Lin, Wei-Lun Tsai |
| 2025 | Fixed Point Certificates for Reachability and Expected Rewards in MDPs. | Krishnendu Chatterjee, Tim Quatmann, Maximilian Schffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken |
| 2025 | Value Iteration with Guessing for Markov Chains and Markov Decision Processes. | Krishnendu Chatterjee, Mahdi JafariRaviz, Raimundo Saona, Jakub Svoboda |
| 2025 | Refuting Equivalence in Probabilistic Programs with Conditioning. | Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotn, Dorde Zikelic |
| 2025 | BUBAAK: Dynamic Cooperative Verification - (Competition Contribution). | Marek Chalupa, Cedric Richter |
| 2025 | Automating the Analysis of Quantitative Automata with QuAK. | Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2025 | Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation. | Daimy Van Caudenberg, Bart Bogaerts, Leandro Vendramin |
| 2025 | Fast value iteration: A uniform approach to efficient algorithms for energy games. | Michal Cadilhac, Antonio Casares, Pierre Ohlmann |
| 2025 | Sound Statistical Model Checking for Probabilities and Expected Rewards. | Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhft |
| 2025 | Weakly Acyclic Diagrams: A Data Structure for Infinite-State Symbolic Verification. | Michael Blondin, Michal Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza, Jakob Schulz |