LOGO
Formal Methods in
Computer-Aided Design
Prague, Czech Republic
October 14 - 18, 2024
FMCAD 2024

Program

Monday, October 14th

The full program is available here: VSTTE Program.

08:30 ­­– 8:55 Registration
08:55 ­­– 9:00 Opening
Session 1
09:00 ­­– 10:00 Symbolic Execution Analysis: Between Testing and Verification Cristian Cadar
10:00 ­­– 10:30 Verifying the Rust Standard Library (Invited Paper) Rahul Kumar, Celina Val, Felipe Monteiro, Michael Tautschnig, Zyad Hassan, Qinheping Hu, Adrian Palacios, Remi Delmas, Jaisurya Nanduri, Felix Klock, Justus Adam, Carolyn Zech, and Artem Agvanian
Coffee Break
Session 2
11:00 ­­– 12:00 High-Assurance Post-Quantum Cryptography Karthikeyan Bhargavan
12:00 ­­– 12:30 Towards Verifying Security Policies for Infinite-State Systems Quentin Peyras, Ghada Gharbi, Souheib Baarir
12:30 ­­– 13:00 MoXIchecker: An Extensible Model Checker for MoXI Salih Ates, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee
Lunch
Session 3
14:30 ­­– 15:30 Pragmatic bounded model checking for TLA+ with Apalache Igor Konnov
15:30 ­­– 16:00 Statically Inferring Usage Bounds for Infrastructure as Code Feitong Qiao, Aryana Mohammadi, Jürgen Cito, Mark Santolucito
16:00 ­­– 16:30 Proof-Producing Symbolic Execution for P4 Didrik Lundberg, Roberto Guanciale, Mads Dam
Coffee Break
Session 4
17:00 ­­– 17:30 PolySAT: Word-level Bit-vector Reasoning in Z3 Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner, Laura Kovacs
17:30 ­­– 18:00 Deductive Verification of Sparse Sets in Why3 Catherine Dubois
18:00 ­­– 18:05 Concluding Remarks by PC Chairs
VSTTE Welcome Drink
18:30 Meeting point for VSTTE Welcome Drink by hotel reception (optional)
19:00 ­– 20:30 VSTTE Welcome Drink (NH Collection Prague Hotel, Mozartova 1, Prague 5 - upper building, Sky Lounge - 4th floor) Welcome Drink

Tuesday, October 15th

This day is Joint VSTTE/FMCAD Tutorial Day.

08:30 ­­– 9:00 Registration
Morning tutorial: VSTTE
09:00 ­­– 10:30 The Lean Programming Language and Theorem Prover – Part 1 Sebastian Ullrich and Joachim Breitner (KIT)
Coffee Break
11:00 ­­– 12:30 The Lean Programming Language and Theorem Prover – Part 2 Sebastian Ullrich and Joachim Breitner (KIT)
Lunch
Afternoon tutorial: FMCAD
14:00 ­­– 15:30 Writing proofs in Dafny – Part 1 K. Rustan M. Leino
Coffee Break
16:00 ­­– 17:30 Writing proofs in Dafny – Part 2 K. Rustan M. Leino
FMCAD 2024 Welcome Reception
18:00 Meeting point for FMCAD 2024 Welcome Reception by hotel reception (optional)
18:30 ­– 20:30 FMCAD 2024 Welcome Reception (Old Town Hall, Staroměstské Sq. 1/3, Prague 1 - Old Town) Welcome Reception

Wednesday, October 16th

08:30 ­­– 9:00 Registration
Invited Talk
09:00 ­­– 10:00 Tackling Scalability Issues in Bit-Vector Reasoning Aina Niemetz
Coffee Break
SMT Solving and Applications
10:30 ­­– 11:00 Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection Ross Daly, Caleb Donovick, Caleb Terrill, Jack Melchert, Priyanka Raina, Clark Barrett and Pat Hanrahan
11:00 ­­– 11:30 Extending DRAT to SMT S Hitarth, Cayden Codel, Hanna Lachnitt and Bruno Dutertre
11:30 ­­– 12:00 Solving String Constraints with Concatenation Using SAT Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong and Dirk Nowotka
12:00 ­­– 12:15 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
12:15 ­­– 12:30 Modernizing SMT-Based Type Error Localization Max Kopinsky, Brigitte Pientka and Xujie Si
Lunch
Static Analysis
14:00 ­­– 14:30 Context Pruning for More Robust SMT-based Program Verification Yi Zhou, Jay Bosamiya, Jessica Li, Marijn Heule and Bryan Parno
14:30 ­­– 15:00 Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions Eytan Singher and Shachar Itzhaky
15:00 ­­– 15:30 Word Equations as Abstract Domain for String Manipulating Programs Antonina Nepeivoda
Coffee Break
ML in Verification
16:00 ­­– 16:30 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
16:30 ­­– 17:00 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
17:00 ­­– 17:30 Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers Daniel Mendoza, Christopher Hahn and Caroline Trippel

Thursday, October 17th

The lunch break has been extended today to give you the opportunity to participate in the poster session. Additionally, posters will be available for viewing throughout the entire day.

Invited Talk
09:00 ­­– 10:00 Some Adventures in Learning Proving, Instantiation and Synthesis Josef Urban
Coffee Break
Verification 1
10:30 ­­– 11:00 Recomposition: A New Technique for Efficient Compositional Verification Ian Dardik, April Porter and Eunsuk Kang
11:00 ­­– 11:15 Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages Shuvendu Lahiri
11:15 ­­– 11:30 Towards Verification Modulo Theories of asynchronous systems via abstraction refinement Gianluca Redondi, Alessandro Cimatti and Alberto Griggio
11:30 ­­– 12:30 Student Forum Lightning Talks
Lunch (with Posters)
Hardware
14:30 ­­– 15:00 Semi-open-state testing for in-silicon coherent interconnects Jasmin Schult, Ben Fiedler, David Cock and Timothy Roscoe
15:00 ­­– 15:30 Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware Rachel Cleaveland and Caroline Trippel
Coffee Break
Proofs and Certificates
16:00 ­­– 16:30 Translating Pseudo-Boolean Proofs to Clausal Proofs Karthik Nukala, Soumyaditya Choudhuri, Randal Bryant and Marijn Heule
16:30 ­­– 17:00 Verified substitution redundancy checking Cayden Codel, Jeremy Avigad and Marijn Heule
17:00 ­­– 17:30 Hardware Model Checking Competition 2024
17:30 ­­– 18:30 Business Meeting
FMCAD Conference Dinner
19:00 Meeting point for FMCAD Conference Dinner by hotel reception (optional)
19:30 ­– 22:30 FMCAD Conference Dinner (Staropramen building, Potrefená husa Restaurant entrance, Paspův Hall on 1. floor, Nádražní 84, Praha 5 - Smichov) Conference Dinner

Friday, October 18th

Invited Talk
09:00 ­­– 10:00 Harnessing SMT Solvers for Reasoning about DeFi Protocols Mooly Sagiv
Coffee Break
SAT Solving and Applications
10:30 ­­– 11:00 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
11:00 ­­– 11:30 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
11:30 ­­– 12:00 Toward Exhaustive Sequential Redundancy Removal Rohit Dureja, Jason Baumgartner, Raj Kumar Gajavelly, Robert Kanzelman and Kristin Yvonne Rozier
12:00 ­­– 12:15 DAG-Based Compositional Approaches for LTLf to DFA Conversions Yash Kankariya, Yong Li and Suguman Bansal
12:15 ­­– 12:30 Clausal Equivalence Sweeping Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Froleyks
Lunch
Algorithms and Arithmetic
14:00 ­­– 14:30 Automatic Verification of Right-greedy Numerical Linear Algebra Algorithms Carl Kwan and Warren Hunt
14:30 ­­– 15:00 Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché and Raphaël Rieu-Helft
15:00 ­­– 15:30 Symbolic Computer Algebra for Multipliers Revisited - It's All About Orders and Phases Alexander Konrad and Christoph Scholl
Coffee Break
Verification 2
16:00 ­­– 16:30 Combining Symbolic Execution with Predicate Abstraction and CEGAR Martin Jonáš, Jan Strejček and Alberto Griggio
16:30 ­­– 17:00 Efficient Synthesis of Symbolic Distributed Protocols by Sketching Derek Egolf, William Schultz and Stavros Tripakis
17:00 ­­– 17:30 Ownership in low-level intermediate representation Siddharth Priya and Arie Gurfinkel