| 2025 | Unlocking Hardware Verification with Oracle Guided Synthesis. | Leiqi Ye, Yixuan Li, Guy Frankel, Jianyi Cheng, Elizabeth Polgreen |
| 2025 | Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models. | Yuan Xia, Aabha Shailesh Pingle, Deepayan Sur, Srivatsan Ravi, Mukund Raghothaman, Jyotirmoy V. Deshmukh |
| 2025 | Per-Instance Subproblem Generation for Strategy Selection in SMT. | Amalee Wilson, Nina Narodytska, Clark W. Barrett, Haoze Wu |
| 2025 | Static Coverage in Deductive Software Verification. | Aaron Tomb, Anjali Joshi |
| 2025 | Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision. | Samuel Teuber, Debasmita Lohar, Bernhard Beckert |
| 2025 | A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SEABMC. | Joseph Tafese, Siddharth Priya, Giuliano Losa, Arie Gurfinkel, Graydon Hoare |
| 2025 | Quantifying Robustness of Medical Image Segmentation Networks Using TensorStars. | Meghan Stuart, Parasara Sridhar Duggirala |
| 2025 | Automated Formal Verification of a Software Fault Isolation System. | Matthew Sotoudeh, Zachary Yedidia |
| 2025 | A Method for the Verification of Memory Management Software in the Presence of TLBs. | Yahya Sohail, Warren A. Hunt Jr. |
| 2025 | Learning Short Clauses via Conditional Autarkies. | Amar Shah, Twain Byrnes, Joseph E. Reeves, Marijn J. H. Heule |
| 2025 | The FMCAD 2025 Student Forum. | Tanja Schindler, Lee Barnett |
| 2025 | "How Does my Circuit Work?": Local Explanations for the Behavior of Sequential Circuits. | Amirmohammad Nazari, Matin Amini, Mukund Raghothaman |
| 2025 | Integrating Large Language Models in Automated Program Verification. | Nina Narodytska |
| 2025 | Solving Set Constraints with Comprehensions and Bounded Quantifiers. | Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik |
| 2025 | Automated Translation Validation of a Compiler for Statically Scheduled Accelerators. | Jackson Melchert, Caleb Terrill, Aron Ricardo Perez-Lopez, Clark W. Barrett, Priyanka Raina |
| 2025 | s2s: An Eager SMT Solver for Strings. | Kevin Lotz, Mitja Kulczynski, Dirk Nowotka |
| 2025 | A Formal Y86 Simulator with CHERI Features. | Carl Kwan, Yutong Xin, William D. Young |
| 2025 | FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits. | Alexander Konrad, Christoph Scholl |
| 2025 | Can Large Language Models Autoformalize Kinematics? | Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch, Andr Platzer |
| 2025 | Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding. | Christopher Johannsen, Phillip H. Jones, Kristin Yvonne Rozier, Tichakorn Wongpiromsarn |
| 2025 | Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols. | Petra Hozzov, Nikolaj S. Bjrner |
| 2025 | OSTRICH2: Solver for Complex String Constraints. | Matthew Hague, Denghang Hu, Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rmmer, Zhilin Wu |
| 2025 | Verification Modulo Theories. | Alberto Griggio |
| 2025 | Systems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods. | Ankush Desai |
| 2025 | PolyVer: A Compositional Approach for Polyglot System Modeling and Verification. | Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia |