| 2024 | 2-DQBF Solving and Certification via Property-Directed Reachability Analysis. Long-Hin Fung, Che Cheng, Yu-Wei Fan, Tony Tan, Jie-Hong Roland Jiang |
| 2024 | Automatic Verification of Right-Greedy Numerical Linear Algebra Algorithms. Carl Kwan, Warren A. Hunt Jr. |
| 2024 | Clausal Equivalence Sweeping. Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks |
| 2024 | Combining Symbolic Execution with Predicate Abstraction and CEGAR. Martin Jonás, Jan Strejcek, Alberto Griggio |
| 2024 | Context Pruning for More Robust SMT-based Program Verification. Yi Zhou, Jay Bosamiya, Jessica Li, Marijn J. H. Heule, Bryan Parno |
| 2024 | DAG-Based Compositional Approaches for LTLf to DFA Conversions. Suguman Bansal, Yash Kankariya, Yong Li |
| 2024 | Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions. Eytan Singher, Shachar Itzhaky |
| 2024 | Efficient Synthesis of Symbolic Distributed Protocols by Sketching. Derek Egolf, William Schultz, Stavros Tripakis |
| 2024 | Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection. Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark W. Barrett, Pat Hanrahan |
| 2024 | Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. Shuvendu K. Lahiri |
| 2024 | Extending DRAT to SMT. S. Hitarth, Cayden R. Codel, Hanna Lachnitt, Bruno Dutertre |
| 2024 | Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024 Nina Narodytska, Philipp Rümmer |
| 2024 | Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function. Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft |
| 2024 | Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark W. Barrett |
| 2024 | Hardware Model Checking Competition 2024. Armin Biere, Nils Froleyks, Mathias Preiner |
| 2024 | Harnessing SMT Solvers for Reasoning about DeFi Protocols. Mooly Sagiv |
| 2024 | Leveraging LLMs for Program Verification. Adharsh Kamath, J. Nausheen Mohammed, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma |
| 2024 | Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware. Rachel Cleaveland, Caroline Trippel |
| 2024 | Modernizing SMT-Based Type Error Localization. Max Kopinsky, Brigitte Pientka, Xujie Si |
| 2024 | Ownership in Low-Level Intermediate Representation. Siddharth Priya, Arie Gurfinkel |
| 2024 | Projective Model Counting for IP Addresses in Access Control Policies. Loris D'Antoni, Andrew Gacek, Amit Goel, Dejan Jovanovic, Rami Gökhan Kici, Daniel Peebles, Neha Rungta, Yasmine Sharoda, Chungha Sung |
| 2024 | Recomposition: A New Technique for Efficient Compositional Verification. Ian Dardik, April Porter, Eunsuk Kang |
| 2024 | SMT-D: New Strategies for Portfolio-Based SMT Solving. Clark W. Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert B. Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Christopher Stephens, Michael W. Whalen |
| 2024 | Semi-Open-State Testing for in-Silicon Coherent Interconnects. Jasmin Schult, Ben Fiedler, David A. Cock, Timothy Roscoe |
| 2024 | Solving String Constraints with Concatenation Using SAT. Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Dirk Nowotka |
| 2024 | Some Adventures in Learning Proving, Instantiation and Synthesis. Josef Urban |
| 2024 | Symbolic Computer Algebra for Multipliers Revisited - It's All About Orders and Phases. Alexander Konrad, Christoph Scholl |
| 2024 | Tackling Scalability Issues in Bit-Vector Reasoning. Aina Niemetz |
| 2024 | The FMCAD 2024 Student Forum. Martin Blicha, Nestan Tsiskaridze |
| 2024 | Toward Exhaustive Sequential Redundancy Removal. Rohit Dureja, Jason Baumgartner, Raj Kumar Gajavelly, Robert Kanzelman, Kristin Y. Rozier |
| 2024 | Towards Verification Modulo Theories of Asynchronous Systems via Abstraction Refinement. Gianluca Redondi, Alessandro Cimatti, Alberto Griggio |
| 2024 | Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers. Daniel Mendoza, Christopher Hahn, Caroline Trippel |
| 2024 | Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs. Karthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J. H. Heule |
| 2024 | Verified Substitution Redundancy Checking. Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2024 | Word Equations as Abstract Domain for String Manipulating Programs. Antonina Nepeivoda |
| 2024 | Writing Proofs in Dafny. K. Rustan M. Leino |