PROCEEDINGS OF THE 25TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2025

Contents

Tutorials
Verification Modulo Theories
Alberto Griggio

Systems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods
Ankush Desai

Invited Talks
Program Synthesis: Pre-LLM and Post-LLM
Ashish Tiwari

Integrating Large Language Models in Automated Program Verification
Nina Narodytska

Student Forum
The FMCAD 2025 Student Forum
Tanja Schindler and Lee Barnett

Hardware Model Checking Competition
Hardware Model Checking Competition 2025
Armin Biere, Nils Froleyks and Mathias Preiner

Temporal Logic
“How Does my Circuit Work?”: Local Explanations for the Behavior of Sequential Circuits
Amirmohammad Nazari, Matin Amini, and Mukund Raghothaman

On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
Raven Beutner and Bernd Finkbeiner

Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding
Christopher Johannsen, Phillip H. Jones, Kristin Yvonne Rozier and Tichakorn Wongpiromsarn

Neural Networks and Large Language Models
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

Quantifying Robustness of Medical Image Segmentation Networks Using TensorStars
Meghan Stuart and Parasara Sridhar Duggirala

Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Samuel Teuber, Debasmita Lohar, and Bernhard Beckert

Can Large Language Models Autoformalize Kinematics?
Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch and André Platzer

SAT and SMT
Towards SMT Solver Stability via Input Normalization
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli and Clark Barrett

Per-Instance Subproblem Generation for Strategy Selection in SMT
Amalee Wilson, Nina Narodytska, Clark Barrett and Haoze Wu

Solving Set Constraints with Comprehensions and Bounded Quantifiers
Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Marsha Chechik

Learning Short Clauses via Conditional Autarkies
Amar Shah, Twain Byrnes, Joseph Reeves and Marijn J. H. Heule

Tools
R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor
Alexis Aurandt, Kristin Yvonne Rozier and Phillip H. Jones

s2s: An Eager SMT Solver for Strings
Kevin Lotz, Mitja Kulczynski and Dirk Nowotka

FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits
Alexander Konrad and Christoph Scholl

OSTRICH2: Solver for Complex String Constraints
Matthew Hague, Denghang Hu, Artur Jeż, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu

Case Studies
A Formal Y86 Simulator with CHERI Features
Carl Kwan, Yutong Xin and William D. Young

A Method for the Verification of Memory Management Software in the Presence of TLBs
Yahya Sohail and Warren A. Hunt, Jr.

Verification Application
Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops
Sewon Park and Atsushi Igarashi

Modeling the AWS Authorization Engine
Lee A. Barnett, Loris D’Antoni, Amit Goel, Rami Gökhan Kici, Neha Rungta, Mary Southern and Chungha Sung

Automated Translation Validation of a Compiler for Statically Scheduled Accelerators
Jackson Melchert, Caleb Terrill, Aron Ricardo Perez-Lopez, Clark Barrett and Priyanka Raina

Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications
Ilo Chen, Che Cheng and Jie-Hong Roland Jiang

Synthesis
Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
Petra Hozzová, Nikolaj Bjørner

Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models
Yuan Xia, Aabha Shailesh Pingle, Deepayan Sur, Srivatsan Ravi, Mukund Raghothaman and Jyotirmoy V. Deshmukh

Unlocking Hardware Verification with Oracle Guided Synthesis
Leiqi Ye, Yixuan Li, Guy Frankel, Jianyi Cheng, and Elizabeth Polgreen

Software Verification
Automated Formal Verification of a Software Fault Isolation System
Matthew Sotoudeh and Zachary Yedidia

Static Coverage in Deductive Software Verification
Aaron Tomb and Anjali Joshi

A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SEABMC
Joseph Tafese, Siddharth Priya, Giuliano Losa, Arie Gurfinkel and Graydon Hoare