Program
Monday, October 14th
The full VSTTE 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) |  |
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) |  |
Wednesday, October 16th
| 08:30 – 9:00 | Registration | |
| Invited Talk | ||
|---|---|---|
| 09:00 – 10:00 | Tackling Scalability Issues in Bit-Vector Reasoning (Slides) | 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 (Slides) | 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) |  |
Friday, October 18th
| Invited Talk | ||
|---|---|---|
| 09:00 – 10:00 | Harnessing SMT Solvers for Reasoning about DeFi Protocols (Slides) | Mooly Sagiv |
| Coffee Break | ||
| SAT Solving and Applications | ||
| 10:30 – 11:00 | 2-DQBF Solving and Certification via Property-Directed Reachability Analysis (Best-Paper Award) | 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 |