PROCEEDINGS OF THE 24TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2024

Contents

Invited Talks
Writing Proofs in Dafny
Rustan M. Leino

Tackling Scalability Issues in Bit-Vector Reasoning
Aina Niemetz

Some Adventures in Learning Proving, Instantiation and Synthesis
Josef Urban

Harnessing SMT Solvers for Reasoning about DeFi Protocols
Mooly Sagiv

Student Forum
The FMCAD 2024 Student Forum
Martin Blicha and Nestan Tsiskaridze

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

SMT Solving and Applications
Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection
Ross Daly, Caleb Donovick, Caleb Terrill, Jack Melchert, Priyanka Raina, Clark Barrett and Pat Hanrahan

Extending DRAT to SMT
Hitarth, Cayden Codel, Hanna Lachnitt and Bruno Dutertre

Solving String Constraints with Concatenation Using SAT
Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong and Dirk Nowotka

SMT-D: New Strategies for Portfolio-Based SMT Solving
Clark Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert Jones, Nham Le, Andrew Reynolds, Kunal Sheth and Mike Whalen

Modernizing SMT-Based Type Error Localization
Max Kopinsky, Brigitte Pientka and Xujie Si

Static Analysis
Context Pruning for More Robust SMT-based Program Verification
Yi Zhou, Jay Bosamiya, Jessica Li, Marijn Heule and Bryan Parno

Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions
Eytan Singher and Shachar Itzhaky

Word Equations as Abstract Domain for String Manipulating Programs
Antonina Nepeivoda

Machine Learning in Verification
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Newell, Umberto Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz and Clark Barrett

Leveraging LLMs for Program Verification
Adharsh Kamath, Nausheen Mohammed, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy and Rahul Sharma

Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers
Daniel Mendoza, Christopher Hahn and Caroline Trippel

Verification I
Recomposition: A New Technique for Efficient Compositional Verification
Ian Dardik, April Porter and Eunsuk Kang

Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
Shuvendu Lahiri

Towards Verification Modulo Theories of asynchronous systems via abstraction refinement
Gianluca Redondi, Alessandro Cimatti and Alberto Griggio

Hardware
Semi-open-state testing for in-silicon coherent interconnects
Jasmin Schult, Ben Fiedler, David Cock and Timothy Roscoe

Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware
Rachel Cleaveland and Caroline Trippel

Proofs and Certificates
Translating Pseudo-Boolean Proofs to Clausal Proofs
Karthik Nukala, Soumyaditya Choudhuri, Randal Bryant and Marijn Heule

Verified substitution redundancy checking
Cayden Codel, Jeremy Avigad and Marijn Heule

Satisfiability Solving and Applications
2-DQBF Solving and Certification via Property-Directed Reachability Analysis
Long-Hin Fung, Che Cheng, Yu-Wei Fan, Tony Tan and Jie-Hong Roland Jiang

Projective Model Counting for IP Addresses in Access Control Policies
Loris D’Antoni, Andrew Gacek, Amit Goel, Dejan Jovanovic, Dan Peebles, Neha Rungta and Yasmine Sharoda

Toward Exhaustive Sequential Redundancy Removal
Rohit Dureja, Jason Baumgartner, Raj Kumar Gajavelly, Robert Kanzelman and Kristin Yvonne Rozier

DAG-Based Compositional Approaches for LTLf to DFA Conversions
Yash Kankariya, Yong Li and Suguman Bansal

Clausal Equivalence Sweeping
Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Froleyks

Algorithms and Arithmetic
Automatic Verification of Right-greedy Numerical Linear Algebra Algorithms
Carl Kwan and Warren Hunt

Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function
Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché and Raphaël Rieu-Helft

Symbolic Computer Algebra for Multipliers Revisited – It’s All About Orders and Phases
Alexander Konrad and Christoph Scholl

Verification II
Combining Symbolic Execution with Predicate Abstraction and CEGAR
Martin Jonáš, Jan Strejček and Alberto Griggio

Efficient Synthesis of Symbolic Distributed Protocols by Sketching
Derek Egolf, William Schultz and Stavros Tripakis

Ownership in low-level intermediate representation
Siddharth Priya and Arie Gurfinkel