TACAS 2026

72 papers

1. A Case Study in Firmware Verification: Applying Formal Methods to Intel$^\circledR $ TDX Module · Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee, Thomas Lemberger
2. A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata · Kyveli Doveri, Pierre Ganty, B. Srivathsan
3. AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic · Valentin Cassano, Pablo F. Castro, Pedro R. D'Argenio, Raul Fervari
4. Automatically Tightening Access Control Policies with Restricter · Ka Lok Wu, Christa Jenkins, Scott D. Stoller, Omar Chowdhury
5. BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability · Jakub Horák, Martin Jonás
6. Bit-Precise Interpolation in Bitwuzla · Aina Niemetz, Mathias Preiner
7. CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems · Roberto Pettinau, Christoph Matheja
8. Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games · Paolo Baldan, Sebastian Gurke, Barbara König, Florian Wittbold
9. Concurrent Permissive Strategy Templates · Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak + 1 more
10. DASA: Fully Gradient-Based Program Analysis (Competition Contribution) · Felix Mächtle, Jan-Niclas Serr, Nils Loose, Thomas Eisenbarth
11. Data Structure Analysis for Binaries · Sadra Bayat Tork, Nicholas Coughlin, Alicia Michael, James Tobler, Kirsten Winter
12. DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling · Francesca Randone, Romina Doz, Mirco Tribastone, Luca Bortolussi
13. Deciding Serializability in Network Systems · Guy Amir, Mark Barbone, Nicolas Amat, Jules Jacobs
14. Deconstructing Subset Construction - Reducing While Determinizing · John Nicol, Markus Frohme
15. Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP · Charles Moloney, Robert Dyer, Elena Sherman
16. Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination · Lukas König, Christian Schildwächter, Michaela Klauck, Christian Heinzemann
17. Efficient Verification of Lingua Franca Programs · Peter Csaba Ölveczky, Mario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin
18. EmergenTheta: Experimental Analyses within the Theta Framework (Competition Contribution) · Milán Mondok, Csanád Telbisz, Levente Bajczi, Dániel Kovács, Mihály Dobos-Kovács, Vince Molnár
19. Enumerating Choice Terms in Model-Based Quantifier Instantiation · Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, Cesare Tinelli
20. Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting · Wei-Jia Huang, Christophe Chareton, Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Alfons Laarman + 1 more
21. Error-Tolerant Quantum State Discrimination: Optimization and Quantum Circuit Synthesis · Chien-Kai Ma, Bo-Hung Chen, Tian-Fu Chen, Dah-Wei Chiou, Jie-Hong R. Jiang
22. Evaluating Software Verifiers for C, Java, and SV-LIB - (Report on SV-COMP 2026) · Dirk Beyer, Jan Strejcek
23. EvolveGen : Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning · Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang
24. Exploring the SMT-LIB Benchmark Library · Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine + 1 more
25. Extending FRET with SLEEC Rules: Formalization, Obligation Inference, and Monitoring · Mahrokh Mirani, Paola Inverardi, Patrizio Pelliccione, Franco Raimondi, Nicolas Troquard
26. Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking) · Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, Georg Zetzsche
27. Faster Signature Refinement for Branching Bisimilarity Minimization · Jan Martens, Maurice Laveaux
28. Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees · Nat Karmios, Sacha-Élie Ayoun, Philippa Gardner
29. Goblint: A Portfolio for Mixed Flow-Sensitive Abstract Interpretation - (Competition Contribution) · Simmo Saan, Ali Rasim Kocal, Michael Petter, Karoliine Holter, Julian Erhard, Michael Schwarz + 2 more
30. Goblitch: Combining Abstract Interpretation with Symbolic Execution via Witnesses - (Competition Contribution) · Karoliine Holter, Paulína Ayaziová, Simmo Saan, Jan Strejcek, Vesal Vojdani
31. Hint-Based SMT Proof Reconstruction · Joshua Clune, Haniel Barbosa, Jeremy Avigad
32. Hornix: From LLVM IR to Constrained Horn Clauses and Back (Competition Contribution) · Martin Blicha, Jan Kofron, Oliver Glitta
33. Iekkë: A SAT-Based Bounded-Round Verifier for Multi-Threaded Programs (Competition Contribution) · Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, Gennaro Parlato
34. Incremental Forward Reasoning for White-Box Proof Search · Xavier Généreux, Jannis Limperg
35. Integrating String Reasoning in Symbolic Execution of C Programs · Rachel Cleaveland, Clark W. Barrett
36. JLiSA: The Java Frontend of the Library for Static Analysis (Competition Contribution) · Vincenzo Arceri, Luca Negrini, Giacomo Zanatta, Filippo Bianchi, Teodors Lisovenko, Luca Olivieri + 1 more
37. LTLf Learning Meets Boolean Set Cover · Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon, Pierre Vandenhove
38. Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob · Dominik Schreiber, Aina Niemetz, Mathias Preiner
39. MightyPPL: Model Checking MITL with Past and Pnueli Modalities · Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh K. Pandya
40. Modular Attractor Acceleration in Infinite-State Games · Philippe Heim, Rayna Dimitrova
41. Mopsa-C: Towards Incorrectness and Termination Verdicts (Competition Contribution) · Marco Milanese, Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné
42. Multiple Long-Run and ømega-Regular Objectives in MDPs · Julius Ide, Joost-Pieter Katoen, Hannah Mertens, Tim Quatmann
43. On Deciding Constant Runtime of Linear Loops · Florian Frohn, Jürgen Giesl, Peter Giesl, Nils Lommen
44. Orbitopal Fixing in SAT · Markus Anders, Cayden R. Codel, Marijn J. H. Heule
45. Parallel SMT Solving via Iterative Tree Partitioning · Tomás Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh, Natasha Sharygina
46. QSOLE: Automatic QBF Equivalence Checking · Peter Pfeiffer, Mark Peyrer, Daniel Große, Martina Seidl
47. Quantifier Elimination Meets Treewidth · Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, Naijun Zhan
48. Re3ver: Reverse and Verify - (Competition Contribution) · Adéla Stepková, Martin Jonás, Jan Strejcek
49. ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics · Makoto Hamana, Kento Emoto
50. ReFuncTion: Conditional Termination by Abstract Interpretation of Numerical C Programs - (Competition Contribution) · Naïm Moussaoui Remil, Caterina Urban
51. ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers · Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang, Cunxi Yu
52. Real-time Proof Checking for Distributed Incremental SAT Solving · Dominik Schreiber, Mathias Fleury, Katalin Fazekas, Armin Biere
53. Revisiting Stateful Partial-Order Reduction · Frédéric Herbreteau, Gérald Point, Gautham Viswanathan, Igor Walukiewicz
54. Robust Verification of Concurrent Stochastic Games · Angel Y. He, David Parker
55. Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing · Chia-Hsuan Lu, Tony Tan, Michael Benedikt
56. SMT(LIA) Sampling with High Diversity · Yong Lai, Junjie Li, Chuan Luo
57. SMTScope: Automated and Efficient Analysis of SMT Traces · Jonás Fiala, Peter Müller
58. SWAT: Improvements to the Symbolic Executor (Competition Contribution) · Nils Loose, Florian Sieck, Felix Mächtle, Thomas Eisenbarth
59. Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities · Ali Rasim Kocal, Michael Schwarz, Simmo Saan, Helmut Seidl
60. Seal: Symbolic Execution with Separation Logic - (Competition Contribution) · Tomás Brablec, Tomás Dacík, Tomás Vojnar
61. Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml · João Madeira Pereira, Filipe Marques, Pedro Adão, Hichem Rami Ait El Hara, Léo Andrès, Arthur Carcano + 4 more
62. Symbiotic 11 Predicate Abstraction Joins the Party - (Competition Contribution) · Paulína Ayaziová, Martin Jonás, Vincent Mihalkovic, Jindrich Sedlácek, Jan Strejcek
63. Syntactically Convex Model-Based Projection for Linear Real Arithmetic · Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel, Lev Nachmanson
64. TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics · S. Akshay, Prerak Contractor, Paul Gastin, R. Govind, B. Srivathsan
65. Trace Repair for Temporal Behavior Trees · Sebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner, Sriram Sankaranarayanan
66. Ultimate Automizer with a One-Dimensional Memory Model - (Competition Contribution) · Manuel Bentele, Max Barth, Marcel Ebbinghaus, Jan Körner, Daniel Dietsch, Matthias Heizmann + 3 more
67. Ultimate Paralizer: Parallel Trace Abstraction (Competition Contribution) · Max Barth, Daniel Dietsch, Matthias Heizmann, Marie-Christine Jakobs
68. VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems · Ludovico Battista, Stefano Tonetta, Gianni Zampedri
69. VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus · Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu + 2 more
70. Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings · Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham
71. Verifying Floating-Point Programs in Stainless · Andrea Gilot, Axel Bergström, Eva Darulova
72. jMT: Testing Correctness of Java Memory Models · Lukas Panneke, Heike Wehrheim