Accepted Papers
Proceedings
The FMCAD'24 proceedings are now available here.
FMCAD 2024 Accepted Papers
| Authors | Title | Comment |
|---|---|---|
| Long-Hin Fung, Che Cheng, Yu-Wei Fan, Tony Tan and Jie-Hong Roland Jiang | 2-DQBF Solving and Certification via Property-Directed Reachability Analysis | Best-paper Award |
| Carl Kwan and Warren Hunt | Automatic Verification of Right-greedy Numerical Linear Algebra Algorithms | |
| Shuvendu Lahiri | Benchmarking LLM-driven User-Intent Formalization for Verification-Aware Languages (short paper) | |
| Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Froleyks | Clausal Equivalence Sweeping (short paper) | |
| Martin Jonáš, Jan Strejček and Alberto Griggio | Combining Symbolic Execution with Predicate Abstraction and CEGAR | |
| Yi Zhou, Jay Bosamiya, Jessica Li, Marijn Heule and Bryan Parno | Context Pruning for More Robust SMT-based Program Verification | |
| Clark Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Mike Whalen and Chriss Stephens | SMT-D: New Strategies for Portfolio-Based SMT Solving (tool paper) | |
| Yash Kankariya, Yong Li and Suguman Bansal | DAG-Based Compositional Approaches for LTLf to DFA Conversions (tool paper) | |
| Eytan Singher and Shachar Itzhaky | Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions | |
| Derek Egolf, William Schultz and Stavros Tripakis | Efficient Synthesis of Symbolic Distributed Protocols by Sketching | |
| Ross Daly, Caleb Donovick, Caleb Terrill, Jack Melchert, Priyanka Raina, Clark Barrett and Pat Hanrahan | Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection | |
| Jasmin Schult, Ben Fiedler, David Cock and Timothy Roscoe | Extended open-state testing for in-silicon coherent interconnects | |
| S Hitarth, Cayden Codel, Hanna Lachnitt and Bruno Dutertre | Extending DRAT to SMT | |
| Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché and Raphaël Rieu-Helft | Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function | |
| 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 | Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates | |
| Adharsh Kamath, Nausheen Mohammed, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy and Rahul Sharma | Leveraging LLMs for Program Verification | |
| Rachel Cleaveland and Caroline Trippel | Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware | |
| Max Kopinsky, Brigitte Pientka and Xujie Si | Modernizing SMT-Based Type Error Localization (tool paper) | |
| Siddharth Priya and Arie Gurfinkel | Ownership in low-level intermediate representation | |
| Loris D'Antoni, Andrew Gacek, Amit Goel, Dejan Jovanovic, Dan Peebles, Neha Rungta and Yasmine Sharoda | Projective Model Counting for IP Addresses in Access Control Policies | |
| Ian Dardik, April Porter and Eunsuk Kang | Recomposition: A New Technique for Efficient Compositional Verification | |
| Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong and Dirk Nowotka | Solving String Constraints with Concatenation Using SAT | |
| Alexander Konrad and Christoph Scholl | Symbolic Computer Algebra for Multipliers Revisited - It's All About Orders and Phases | |
| Rohit Dureja, Jason Baumgartner, Raj Kumar Gajavelly, Robert Kanzelman and Kristin Yvonne Rozier | Toward Exhaustive Sequential Redundancy Removal | |
| Gianluca Redondi, Alessandro Cimatti and Alberto Griggio | Towards Verification Modulo Theories of asynchronous systems via abstraction refinement (short paper) | |
| Daniel Mendoza, Christopher Hahn and Caroline Trippel | Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers | |
| Karthik Nukala, Soumyaditya Choudhuri, Randal Bryant and Marijn Heule | Translating Pseudo-Boolean Proofs to Clausal Proofs | |
| Cayden Codel, Jeremy Avigad and Marijn Heule | Verified substitution redundancy checking | |
| Antonina Nepeivoda | Word Equations as Abstract Domain for String Manipulating Programs |