PROCEEDINGS OF THE 25TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2025
Conference Series: Formal Methods in Computer-Aided Design, Band 6
Beiträge
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
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
Produktinformationen
Erschienen: Oktober 2025Umfang: 286 Seiten
Format: 24 x 17 cm
Sprache: Englisch
DOI: 10.34727/2025/isbn.978-3-85448-084-6
ISBN (E-Book): 978-3-85448-084-6