TACAS 2025

60 papers

1. AISE v2.0: Combining Loop Transformations - (Competition Contribution) · Yao Lin, Zhenbang Chen, Ji Wang
2. AProVE(KoAT+LoAT) - (Competition Contribution) · Nils Lommen, Jürgen Giesl
3. Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction · Derek Egolf, Stavros Tripakis
4. Augmenting Model-Based Instantiation with Fast Enumeration · Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette
5. 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 Lengál, Jyun-Ao Lin + 1 more
6. Automated Analysis of Logically Constrained Rewrite Systems using crest · Jonas Schöpf, Aart Middeldorp
7. Automating the Analysis of Quantitative Automata with QuAK · Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç
8. BUBAAK: Dynamic Cooperative Verification - (Competition Contribution) · Marek Chalupa, Cedric Richter
9. CPAchecker 4.0 as Witness Validator - (Competition Contribution) · Dirk Beyer, Marian Lingsch Rosenfeld
10. Certifiably Robust Policies for Uncertain Parametric Environments · Yannik Schnitzer, Alessandro Abate, David Parker
11. Certifying Pareto-Optimality in Multi Objective Maximum Satisfiability · Christoph Jabs, Jeremias Berg, Bart Bogaerts, Matti Järvisalo
12. Cyclone: A Heterogeneous Tool for Verifying Infinite Descent · Liron Cohen, Reuben N. S. Rowe, Matan Shaked
13. D-Painless: A Framework for Distributed Portfolio SAT Solving · Mazigh Saoudi, Souheib Baarir, Julien Sopena, Thibault Lejemble
14. Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM · Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym, Jan Midtgaard
15. ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction - (Competition Contribution) · Tong Wu, Xianzhiyu Li, Edoardo Manino, Rafael Sá Menezes, Mikhail R. Gadelha, Shale Xiong + 3 more
16. Efficient Evidence Generation for Modal μ-Calculus Model Checking · Anna Stramaglia, Jeroen J. A. Keiren, Maurice Laveaux, Tim A. C. Willemse
17. EmergenTheta: Variations on Symbolic Transition Systems (Competition Contribution) · Milán Mondok, Levente Bajczi, Dániel Szekeres, Vince Molnár
18. Equivalence Checking of a libm Port · Mark Baranowski, Zvonimir Rakamaric, Ganesh Gopalakrishnan
19. Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs · Daniela Kaufmann, Jérémy Berthomieu
20. Fast value iteration: A uniform approach to efficient algorithms for energy games · Michaël Cadilhac, Antonio Casares, Pierre Ohlmann
21. Fixed Point Certificates for Reachability and Expected Rewards in MDPs · Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken
22. Formally Verifying a Transformation from MLTL Formulas to Regular Expressions · Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier
23. GPUexploresc prob: Markov Chain State Space Construction and Verification with GPUs · Jan Heemstra, Anton Wijs
24. Implicit Rankings for Verifying Liveness Properties in First-Order Logic · Raz Lotan, Sharon Shoham
25. Improvements in Software Verification and Witness Validation: SV-COMP 2025 · Dirk Beyer, Jan Strejcek
26. Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation · Daimy Van Caudenberg, Bart Bogaerts, Leandro Vendramin
27. Inferring Incorrectness Specifications for Object-Oriented Programs · Wenhua Li, Quang Loc Le, Yahui Song, Wei-Ngan Chin
28. Learning Real-Time One-Counter Automata Using Polynomially Many Queries · Prince Mathew, Vincent Penelle, A. V. Sreejith
29. LydiaSyft: A Compositional Symbolic Synthesis Framework for LTLf Specifications · Shufang Zhu, Marco Favorito
30. Mopsa-C with Trace Partitioning and Autosuggestions (Competition Contribution) · Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné
31. Multiparty Session Typing, Embedded · Sung-Shik Jongmans
32. Nacpa: Native Checking with Parallel-Portfolio Analyses - (Competition Contribution) · Thomas Lemberger, Henrik Wachowitz
33. Neural Network Verification with Branch-and-Bound for General Nonlinearities · Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, Huan Zhang
34. Non-Zero-Sum Games with Multiple Weighted Objectives · Yoav Feinstein, Orna Kupferman, Noam Shenwald
35. On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study) · Levente Bajczi, Csanád Telbisz, Dániel Szekeres, András Vörös
36. PROTON 2.1: Synthesizing Ranking Functions via fine-tuned locally Hosted LLM (Competition Contribution) · Diganta Mukhopadhyay, Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar
37. Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 · Leni Aniva, Chuyue Sun, Brando Miranda, Clark W. Barrett, Sanmi Koyejo
38. Parallel Equivalence Checking of Stabilizer Quantum Circuits on GPUs · Muhammad Osama, Dimitrios Thanos, Alfons Laarman
39. Performance Heuristics for GR(1) Realizability Checking and Related Analyses · Roy Yatskan, Ilia Shevrin, Shahar Maoz
40. Proxy Attribute Discovery in Machine Learning Datasets via Inductive Logic Programming · Rafael Gonçalves, Filipe Gouveia, Inês Lynce, José Fragoso Santos
41. Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions · Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu, David A. Basin
42. RacerF: Data Race Detection with Frama-C (Competition Contribution) · Tomás Dacík, Tomás Vojnar
43. Reachability for Nonsmooth Systems with Lexicographic Jacobians · Chenxi Ji, Huan Zhang, Sayan Mitra
44. Refuting Equivalence in Probabilistic Programs with Conditioning · Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Dorde Zikelic
45. Revisiting DRUP-Based Interpolants with CaDiCaL 2.0 · Basel Khouri, Yakir Vizel
46. Revisiting Differential Verification: Equivalence Verification with Confidence · Samuel Teuber, Philipp Kern, Marvin Janzen, Bernhard Beckert
47. SV-COMP'25 Reproduction Report (Competition Contribution) · Levente Bajczi, Zsófia Ádám, Zoltán Micskei
48. SVF-SVC: Software Verification Using SVF (Competition Contribution) · Cameron McGowan, Matthew Richards, Yulei Sui
49. SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning · Jan Kretínský, Tobias Meggendorfer, Maximilian Prokop, Ashkan Zarkhah
50. SliQSim: A Quantum Circuit Simulator and Solver for Probability and Statistics Queries · Tian-Fu Chen, Jie-Hong R. Jiang
51. Sound Statistical Model Checking for Probabilities and Expected Rewards · Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft
52. Stream-Based Monitoring of Algorithmic Fairness · Jan Baumeister, Bernd Finkbeiner, Frederik Scheerer, Julian Siber, Tobias Wagenpfeil
53. Synthesis of Universal Safety Controllers · Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak, Anne-Kathrin Schmuck
54. Synthesis with Guided Environments · Orna Kupferman, Ofer Leshkowitz
55. Theta: Various Approaches for Concurrent Program Verification (Competition Contribution) · Csanád Telbisz, Levente Bajczi, Dániel Szekeres, András Vörös
56. Token Elimination in Model Checking of Petri Nets · Nicolaj Ø. Jensen, Kim G. Larsen, Jirí Srba
57. Unsatisfiability Proofs for Horn Solving · Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofron, Natasha Sharygina
58. Value Iteration with Guessing for Markov Chains and Markov Decision Processes · Krishnendu Chatterjee, Mahdi JafariRaviz, Raimundo Saona, Jakub Svoboda
59. Weakly Acyclic Diagrams: A Data Structure for Infinite-State Symbolic Verification · Michael Blondin, Michaël Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza, Jakob Schulz
60. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation · David Chocholatý, Vojtech Havlena, Lukás Holík, Jan Hranicka, Ondrej Lengál, Juraj Síc