| 2025 | "How Does my Circuit Work?": Local Explanations for the Behavior of Sequential Circuits. Amirmohammad Nazari, Matin Amini, Mukund Raghothaman |
| 2025 | A Formal Y86 Simulator with CHERI Features. Carl Kwan, Yutong Xin, William D. Young |
| 2025 | A Method for the Verification of Memory Management Software in the Presence of TLBs. Yahya Sohail, Warren A. Hunt Jr. |
| 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 | Automated Formal Verification of a Software Fault Isolation System. Matthew Sotoudeh, Zachary Yedidia |
| 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 | Can Large Language Models Autoformalize Kinematics? Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch, André Platzer |
| 2025 | FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits. Alexander Konrad, Christoph Scholl |
| 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 | Hardware Model Checking Competition 2025. Armin Biere, Nils Froleyks, Mathias Preiner |
| 2025 | Integrating Large Language Models in Automated Program Verification. Nina Narodytska |
| 2025 | Learning Short Clauses via Conditional Autarkies. Amar Shah, Twain Byrnes, Joseph E. Reeves, Marijn J. H. Heule |
| 2025 | Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops. Sewon Park, Atsushi Igarashi |
| 2025 | Modeling the AWS Authorization Engine. Lee A. Barnett, Loris D'Antoni, Amit Goel, Rami Gökhan Kici, Neha Rungta, Mary Southern, Chungha Sung |
| 2025 | OSTRICH2: Solver for Complex String Constraints. Matthew Hague, Denghang Hu, Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu |
| 2025 | Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision. Samuel Teuber, Debasmita Lohar, Bernhard Beckert |
| 2025 | On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information. Raven Beutner, Bernd Finkbeiner |
| 2025 | Per-Instance Subproblem Generation for Strategy Selection in SMT. Amalee Wilson, Nina Narodytska, Clark W. Barrett, Haoze Wu |
| 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 |
| 2025 | Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025 Ahmed Irfan, Daniela Kaufmann |
| 2025 | Program Synthesis: Pre-LLM and Post-LLM. Ashish Tiwari |
| 2025 | Quantifying Robustness of Medical Image Segmentation Networks Using TensorStars. Meghan Stuart, Parasara Sridhar Duggirala |
| 2025 | R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor. Alexis A. Aurandt, Kristin Yvonne Rozier, Phillip H. Jones |
| 2025 | Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding. Christopher Johannsen, Phillip H. Jones, Kristin Yvonne Rozier, Tichakorn Wongpiromsarn |
| 2025 | Solving Set Constraints with Comprehensions and Bounded Quantifiers. Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik |
| 2025 | Static Coverage in Deductive Software Verification. Aaron Tomb, Anjali Joshi |
| 2025 | Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols. Petra Hozzová, Nikolaj Bjørner |
| 2025 | Systems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods. Ankush Desai |
| 2025 | The FMCAD 2025 Student Forum. Tanja Schindler, Lee Barnett |
| 2025 | Towards SMT Solver Stability via Input Normalization. Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett |
| 2025 | Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications. Ilo Chen, Che Cheng, Jie-Hong Roland Jiang |
| 2025 | Unlocking Hardware Verification with Oracle Guided Synthesis. Leiqi Ye, Yixuan Li, Guy Frankel, Jianyi Cheng, Elizabeth Polgreen |
| 2025 | Verification Modulo Theories. Alberto Griggio |
| 2025 | s2s: An Eager SMT Solver for Strings. Kevin Lotz, Mitja Kulczynski, Dirk Nowotka |