| 2026 | Probabilistic Verification for Modular Network-on-Chip Systems. | Nick Waddoups, Jonah Boe, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, Zhen Zhang |
| 2026 | A Formal Executable Semantics of PROMELA. | Byoungho Son, Kyungmin Bae |
| 2026 | Multi-variable Quantification of BDDs in External Memory using Nested Sweeping. | Steffan Christ Slvsten, Jaco van de Pol |
| 2026 | Data Race Detection by Digest-Driven Abstract Interpretation. | Michael Schwarz, Julian Erhard |
| 2026 | Verification of Generic VHDL Designs and Their Translation to Rocq. | Ocan Sankur, Benot Boyer, Florian Faissole |
| 2026 | Termination Resilience Static Analysis. | Nam Moussaoui Remil, Caterina Urban |
| 2026 | Efficient Discovery of Actual Causality in Stochastic Systems. | Arshia Rafieioskouei, Kenneth Rogale, Borzoo Bonakdarpour |
| 2026 | Input-Based Three-Valued Abstraction Refinement. | Jan Onderka, Stefan Ratschan |
| 2026 | Try-Mopsa: Relational Static Analysis in Your Pocket. | Raphal Monat |
| 2026 | SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation. | Junjie Meng, Jie An, Yong Li, Andrea Turrini, Miaomiao Zhang |
| 2026 | Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification. | Andreas Lindner, Karl Palmskog, Scott Constable, Mads Dam, Roberto Guanciale, Hamed Nemati |
| 2026 | Finding Photonics Circuits via δ-Weakening SMT. | Marco Lewis, Benot Valiron |
| 2026 | Proof Minimization in Neural Network Verification. | Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2026 | A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamic Systems. | Rui Guo, Yang Li, Xiuqing Cao, Wang Lin |
| 2026 | Atomic Gliders and Cellular Automata as Language Generators. | Dana Fisman, Noa Izsak |
| 2026 | Efficiently Verifying Quantum Programs with Few T Gates. | Youngchan Cho, Robert Rand |
| 2026 | Reachability in Multi-agent Transfer Systems. | Nathalie Bertrand, Loc Hlout, Engel Lefaucheux, Luca Paparazzo |
| 2026 | Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver. | Bruno Andreotti, Haniel Barbosa |
| 2025 | Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications. | Ruoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi |
| 2025 | Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training. | Junfeng Yang, Min Zhang, Xin Chen, Qin Li |
| 2025 | Discovering Likely Invariants for Distributed Systems Through Runtime Monitoring and Learning. | Yuan Xia, Deepayan Sur, Aabha Shailesh Pingle, Jyotirmoy V. Deshmukh, Mukund Raghothaman, Srivatsan Ravi |
| 2025 | Automated Flaw Detection for Industrial Robot RESTful Service. | Yuncheng Wang, Puzhuo Liu, Yaowen Zheng, Dongliang Fang, Shuaizong Si, Zhiwen Pan, Weidong Zhang, Limin Sun |
| 2025 | Automatic Inference of Relational Object Invariants. | Yusen Su, Jorge A. Navas, Arie Gurfinkel, Isabel Garcia-Contreras |
| 2025 | Property-Agnostic Base Case Extension for Scalable Verification of Distributed Systems. | Kyle Storey, Eric Mercer |
| 2025 | An Abstract Domain for Heap Commutativity. | Jared Pincus, Eric Koskinen |