| 2026 | A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata. | Kyveli Doveri, Pierre Ganty, B. Srivathsan |
| 2026 | Hint-Based SMT Proof Reconstruction. | Joshua Clune, Haniel Barbosa, Jeremy Avigad |
| 2026 | Integrating String Reasoning in Symbolic Execution of C Programs. | Rachel Cleaveland, Clark W. Barrett |
| 2026 | ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers. | Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang, Cunxi Yu |
| 2026 | AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic. | Valentin Cassano, Pablo F. Castro, Pedro R. D'Argenio, Raul Fervari |
| 2026 | Seal: Symbolic Execution with Separation Logic - (Competition Contribution). | Toms Brablec, Toms Dack, Toms Vojnar |
| 2026 | Hornix: From LLVM IR to Constrained Horn Clauses and Back (Competition Contribution). | Martin Blicha, Jan Kofron, Oliver Glitta |
| 2026 | 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 |
| 2026 | Evaluating Software Verifiers for C, Java, and SV-LIB - (Report on SV-COMP 2026). | Dirk Beyer, Jan Strejcek |
| 2026 | 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 |
| 2026 | Ultimate Automizer with a One-Dimensional Memory Model - (Competition Contribution). | Manuel Bentele, Max Barth, Marcel Ebbinghaus, Jan Krner, Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schssele, Andreas Podelski |
| 2026 | Syntactically Convex Model-Based Projection for Linear Real Arithmetic. | Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel, Lev Nachmanson |
| 2026 | VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems. | Ludovico Battista, Stefano Tonetta, Gianni Zampedri |
| 2026 | LTL | Gabriel Bathie, Nathanal Fijalkow, Tho Matricon, Baptiste Mouillon, Pierre Vandenhove |
| 2026 | Ultimate Paralizer: Parallel Trace Abstraction (Competition Contribution). | Max Barth, Daniel Dietsch, Matthias Heizmann, Marie-Christine Jakobs |
| 2026 | Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games. | Paolo Baldan, Sebastian Gurke, Barbara Knig, Florian Wittbold |
| 2026 | Symbiotic 11 Predicate Abstraction Joins the Party - (Competition Contribution). | Paulna Ayaziov, Martin Jons, Vincent Mihalkovic, Jindrich Sedlcek, Jan Strejcek |
| 2026 | JLiSA: The Java Frontend of the Library for Static Analysis (Competition Contribution). | Vincenzo Arceri, Luca Negrini, Giacomo Zanatta, Filippo Bianchi, Teodors Lisovenko, Luca Olivieri, Pietro Ferrara |
| 2026 | Orbitopal Fixing in SAT. | Markus Anders, Cayden R. Codel, Marijn J. H. Heule |
| 2026 | Concurrent Permissive Strategy Templates. | Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klppelholz, Ali Mirzaei, Satya Prakash Nayak, Anne-Kathrin Schmuck |
| 2026 | Deciding Serializability in Network Systems. | Guy Amir, Mark Barbone, Nicolas Amat, Jules Jacobs |
| 2026 | TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics. | S. Akshay, Prerak Contractor, Paul Gastin, R. Govind, B. Srivathsan |
| 2025 | LydiaSyft: A Compositional Symbolic Synthesis Framework for LTL | Shufang Zhu, Marco Favorito |
| 2025 | Performance Heuristics for GR(1) Realizability Checking and Related Analyses. | Roy Yatskan, Ilia Shevrin, Shahar Maoz |
| 2025 | 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, Norbert Tihanyi, Pavlos Petoumenos, Lucas C. Cordeiro |