| 2025 | Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications. | Ilo Chen, Che Cheng, Jie-Hong Roland Jiang |
| 2025 | Hardware Model Checking Competition 2025. | Armin Biere, Nils Froleyks, Mathias Preiner |
| 2025 | On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information. | Raven Beutner, Bernd Finkbeiner |
| 2025 | Modeling the AWS Authorization Engine. | Lee A. Barnett, Loris D'Antoni, Amit Goel, Rami Gkhan Kici, Neha Rungta, Mary Southern, Chungha Sung |
| 2025 | R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor. | Alexis A. Aurandt, Kristin Yvonne Rozier, Phillip H. Jones |
| 2025 | Towards SMT Solver Stability via Input Normalization. | Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett |
| 2025 | Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops. | Sewon Park, Atsushi Igarashi |
| 2025 | Program Synthesis: Pre-LLM and Post-LLM. | Ashish Tiwari |
| 2024 | Context Pruning for More Robust SMT-based Program Verification. | Yi Zhou, Jay Bosamiya, Jessica Li, Marijn J. H. Heule, Bryan Parno |
| 2024 | Some Adventures in Learning Proving, Instantiation and Synthesis. | Josef Urban |
| 2024 | Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions. | Eytan Singher, Shachar Itzhaky |
| 2024 | Semi-Open-State Testing for in-Silicon Coherent Interconnects. | Jasmin Schult, Ben Fiedler, David A. Cock, Timothy Roscoe |
| 2024 | Harnessing SMT Solvers for Reasoning about DeFi Protocols. | Mooly Sagiv |
| 2024 | Towards Verification Modulo Theories of Asynchronous Systems via Abstraction Refinement. | Gianluca Redondi, Alessandro Cimatti, Alberto Griggio |
| 2024 | Ownership in Low-Level Intermediate Representation. | Siddharth Priya, Arie Gurfinkel |
| 2024 | Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs. | Karthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J. H. Heule |
| 2024 | Tackling Scalability Issues in Bit-Vector Reasoning. | Aina Niemetz |
| 2024 | Word Equations as Abstract Domain for String Manipulating Programs. | Antonina Nepeivoda |
| 2024 | Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers. | Daniel Mendoza, Christopher Hahn, Caroline Trippel |
| 2024 | Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. | Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark W. Barrett |
| 2024 | Solving String Constraints with Concatenation Using SAT. | Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Dirk Nowotka |
| 2024 | Writing Proofs in Dafny. | K. Rustan M. Leino |
| 2024 | Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. | Shuvendu K. Lahiri |
| 2024 | Automatic Verification of Right-Greedy Numerical Linear Algebra Algorithms. | Carl Kwan, Warren A. Hunt Jr. |
| 2024 | Modernizing SMT-Based Type Error Localization. | Max Kopinsky, Brigitte Pientka, Xujie Si |