FMCAD 2025: INTERNATIONAL CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN 2025

A
Amini, Matin	"How Does my Circuit Work?": Local Explanations for the Behavior of Sequential Circuits
Amrollahi, Daneshvar	Towards SMT Solver Stability via Input Normalization
Aurandt, Alexis	R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor
B
Barnett, Lee	Modeling the AWS Authorization Engine Student Forum
Barrett, Clark	Automated Translation Validation of a Compiler for Statically Scheduled Accelerators Towards SMT Solver Stability via Input Normalization Per-Instance Subproblem Generation for Strategy Selection in SMT Solving Set Constraints with Comprehensions and Bounded Quantifiers
Beckert, Bernhard	Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Beutner, Raven	On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
Bharadwaj, Sagar	Can Large Language Models Autoformalize Kinematics?
Biere, Armin	Hardware Model Checking Competition
Bjørner, Nikolaj	Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
Byrnes, Twain	Learning Short Clauses via Conditional Autarkies
C
Charikar, Moses	Towards SMT Solver Stability via Input Normalization
Chechik, Marsha	Solving Set Constraints with Comprehensions and Bounded Quantifiers
Chen, Ilo	Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications
Chen, Pei-Wei	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Cheng, Che	Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications
Cheng, Jianyi	Unlocking Hardware Verification with Oracle Guided Synthesis
D
D'Antoni, Loris	Modeling the AWS Authorization Engine
Desai, Ankush	Systems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods
Deshmukh, Jyotirmoy V.	Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models
Duggirala, Parasara Sridhar	Quantifying Robustness of 3D BioMedical Image Segmentation Networks Using TensorStars
F
Feng, Nick	Solving Set Constraints with Comprehensions and Bounded Quantifiers
Finkbeiner, Bernd	On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
Frankel, Guy	Unlocking Hardware Verification with Oracle Guided Synthesis
Froleyks, Nils	Hardware Model Checking Competition
G
Godbole, Adwait	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Goel, Amit	Modeling the AWS Authorization Engine
Griggio, Alberto	Verification Modulo Theories
Gurfinkel, Arie	A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SeaBMC
H
Hague, Matthew	OSTRICH: Solver for Complex String Constraints
Heule, Marijn J. H.	Learning Short Clauses via Conditional Autarkies
Hoare, Graydon	A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SeaBMC
Hozzová, Petra	Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
Hu, Denghang	OSTRICH: Solver for Complex String Constraints
Hunt, Warren	A Method for the Verification of Memory Management Software in the Presence of TLBs
I
Igarashi, Atsushi	Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops
J
Jeż, Artur	OSTRICH: Solver for Complex String Constraints
Jiang, Jie-Hong R.	Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications
Johannsen, Christopher	Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding
Jones, Phillip H.	R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding
Joshi, Anjali	Static Coverage in Deductive Software Verification
K
Kabra, Aditi	Can Large Language Models Autoformalize Kinematics?
Konrad, Alexander	FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits
Kulczynski, Mitja	s2s: An Eager SMT Solver for Strings
Kwan, Carl	A Formal Y86 Simulator with CHERI Features
Kıcı, Rami Gökhan	Modeling the AWS Authorization Engine
L
Laurent, Jonathan	Can Large Language Models Autoformalize Kinematics?
Lee, Edward	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Li, Yixuan	Unlocking Hardware Verification with Oracle Guided Synthesis
Lin, Anthony W.	OSTRICH: Solver for Complex String Constraints
Lin, Shaokai	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Lohar, Debasmita	Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Losa, Giuliano	A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SeaBMC
Lotz, Kevin	s2s: An Eager SMT Solver for Strings
M
Markgraf, Oliver	OSTRICH: Solver for Complex String Constraints
Martins, Ruben	Can Large Language Models Autoformalize Kinematics?
Melchert, Jackson	Automated Translation Validation of a Compiler for Statically Scheduled Accelerators
Mitsch, Stefan	Can Large Language Models Autoformalize Kinematics?
Mohamed, Mudathir	Solving Set Constraints with Comprehensions and Bounded Quantifiers
N
Narodytska, Nina	Integrating Large Language Models in Automated Program Verification
Narodytska, Nina	Per-Instance Subproblem Generation for Strategy Selection in SMT
Nazari, Amirmohammad	"How Does my Circuit Work?": Local Explanations for the Behavior of Sequential Circuits
Niemetz, Aina	Towards SMT Solver Stability via Input Normalization
Nowotka, Dirk	s2s: An Eager SMT Solver for Strings
P
Park, Sewon	Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops
Pingle, Aabha Shailesh	Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models
Platzer, André	Can Large Language Models Autoformalize Kinematics?
Polgreen, Elizabeth	Unlocking Hardware Verification with Oracle Guided Synthesis PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Preiner, Mathias	Towards SMT Solver Stability via Input Normalization Hardware Model Checking Competition
Priya, Siddharth	A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SeaBMC
R
Raghothaman, Mukund	Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models "How Does my Circuit Work?": Local Explanations for the Behavior of Sequential Circuits
Raina, Priyanka	Automated Translation Validation of a Compiler for Statically Scheduled Accelerators
Ravi, Srivatsan	Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models
Reeves, Joseph	Learning Short Clauses via Conditional Autarkies
Reynolds, Andrew	Towards SMT Solver Stability via Input Normalization Solving Set Constraints with Comprehensions and Bounded Quantifiers
Ricardo Perez-Lopez, Áron	Automated Translation Validation of a Compiler for Statically Scheduled Accelerators
Rozier, Kristin Yvonne	R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding
Rungta, Neha	Modeling the AWS Authorization Engine
Rümmer, Philipp	OSTRICH: Solver for Complex String Constraints
S
Schindler, Tanja	Student Forum
Scholl, Christoph	FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits
Seshia, Sanjit	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Shah, Amar	Learning Short Clauses via Conditional Autarkies
Singh, Ramneet	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Sohail, Yahya	A Method for the Verification of Memory Management Software in the Presence of TLBs
Sotoudeh, Matthew	Automated Formal Verification of a Software Fault Isolation System
Southern, Mary	Modeling the AWS Authorization Engine
Strub, Pierre-Yves	EasyCrypt - Part I EasyCrypt - Part II
Stuart, Meghan	Quantifying Robustness of 3D BioMedical Image Segmentation Networks Using TensorStars
Sung, Chungha	Modeling the AWS Authorization Engine
Sur, Deepayan	Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models
T
Tafese, Joseph	A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SeaBMC
Terrill, Caleb	Automated Translation Validation of a Compiler for Statically Scheduled Accelerators
Teuber, Samuel	Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Tinelli, Cesare	Towards SMT Solver Stability via Input Normalization Solving Set Constraints with Comprehensions and Bounded Quantifiers
Tiwari, Ashish	Program Synthesis: Pre-LLM and Post-LLM
Tomb, Aaron	Static Coverage in Deductive Software Verification
W
Wilson, Amalee	Per-Instance Subproblem Generation for Strategy Selection in SMT
Wongpiromsarn, Tichakorn	Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding
Wu, Haoze	Per-Instance Subproblem Generation for Strategy Selection in SMT
Wu, Zhilin	OSTRICH: Solver for Complex String Constraints
X
Xia, Yuan	Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models
Xin, Yutong	A Formal Y86 Simulator with CHERI Features
Y
Ye, Leiqi	Unlocking Hardware Verification with Oracle Guided Synthesis
Yedidia, Zachary	Automated Formal Verification of a Software Fault Isolation System
Young, William D.	A Formal Y86 Simulator with CHERI Features

Disclaimer | Powered by EasyChair Smart Program