| 2026 | 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 |
| 2026 | Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing. | Chia-Hsuan Lu, Tony Tan, Michael Benedikt |
| 2026 | Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings. | Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham |
| 2026 | SWAT: Improvements to the Symbolic Executor (Competition Contribution). | Nils Loose, Florian Sieck, Felix Mchtle, Thomas Eisenbarth |
| 2026 | Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking). | Kilian Lichtner, Pascal Bergstrer, Moses Ganardi, Anthony W. Lin, Georg Zetzsche |
| 2026 | SMT(LIA) Sampling with High Diversity. | Yong Lai, Junjie Li, Chuan Luo |
| 2026 | Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination. | Lukas Knig, Christian Schildwchter, Michaela Klauck, Christian Heinzemann |
| 2026 | Enumerating Choice Terms in Model-Based Quantifier Instantiation. | Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, Cesare Tinelli |
| 2026 | Parallel SMT Solving via Iterative Tree Partitioning. | Toms Kolrik, Antti E. J. Hyvrinen, Seyedmasoud Asadzadeh, Natasha Sharygina |
| 2026 | Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities. | Ali Rasim Kocal, Michael Schwarz, Simmo Saan, Helmut Seidl |
| 2026 | Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees. | Nat Karmios, Sacha-lie Ayoun, Philippa Gardner |
| 2026 | Multiple Long-Run and mega-Regular Objectives in MDPs. | Julius Ide, Joost-Pieter Katoen, Hannah Mertens, Tim Quatmann |
| 2026 | EvolveGen : Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning. | Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang |
| 2026 | 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, Jingyi Mei |
| 2026 | BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability. | Jakub Hork, Martin Jons |
| 2026 | Goblitch: Combining Abstract Interpretation with Symbolic Execution via Witnesses - (Competition Contribution). | Karoliine Holter, Paulna Ayaziov, Simmo Saan, Jan Strejcek, Vesal Vojdani |
| 2026 | MightyPPL: Model Checking MITL with Past and Pnueli Modalities. | Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh K. Pandya |
| 2026 | Revisiting Stateful Partial-Order Reduction. | Frdric Herbreteau, Grald Point, Gautham Viswanathan, Igor Walukiewicz |
| 2026 | Robust Verification of Concurrent Stochastic Games. | Angel Y. He, David Parker |
| 2026 | Modular Attractor Acceleration in Infinite-State Games. | Philippe Heim, Rayna Dimitrova |
| 2026 | ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics. | Makoto Hamana, Kento Emoto |
| 2026 | Verifying Floating-Point Programs in Stainless. | Andrea Gilot, Axel Bergstrm, Eva Darulova |
| 2026 | Incremental Forward Reasoning for White-Box Proof Search. | Xavier Gnreux, Jannis Limperg |
| 2026 | On Deciding Constant Runtime of Linear Loops. | Florian Frohn, Jrgen Giesl, Peter Giesl, Nils Lommen |
| 2026 | SMTScope: Automated and Efficient Analysis of SMT Traces. | Jons Fiala, Peter Mller |