| 2019 | An Increasing Need for Formality (Keynote). | Martin Dixon |
| 2019 | Synthesizing Reactive Systems Using Robustness and Recovery Specifications. | Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman |
| 2019 | Chasing Minimal Inductive Validity Cores in Hardware Model Checking. | Ryan Berryhill, Andreas G. Veneris |
| 2019 | Concurrent Chaining Hash Maps for Software Model Checking. | Freark I. van der Berg, Jaco van de Pol |
| 2019 | Verifying Relational Properties using Trace Logic. | Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovcs, Matteo Maffei |
| 2019 | Extending enumerative function synthesis via SMT-driven classification. | Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli |
| 2019 | Knowledge Compilation for Boolean Functional Synthesis. | S. Akshay, Jatin Arora, Supratik Chakraborty, Shankara Narayanan Krishna, Divya Raghunathan, Shetal Shah |
| 2018 | ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. | Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Martonosi, Sharad Malik |
| 2018 | Complete and Efficient DRAT Proof Checking. | Adrian Rebola-Pardo, Lus Cruz-Filipe |
| 2018 | Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques. | Vikas Rao, Utkarsh Gupta, Irina Ilioaea, Arpitha Srinath, Priyank Kalla, Florian Enescu |
| 2018 | Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. | Thomas Pani, Georg Weissenbacher, Florian Zuleger |
| 2018 | Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. | Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham |
| 2018 | Deductive Verification of Distributed Protocols in First-Order Logic. | Oded Padon |
| 2018 | Learning Linear Temporal Properties. | Daniel Neider, Ivan Gavran |
| 2018 | Formal Verification of Deep Neural Networks. | Nina Narodytska |
| 2018 | CoSA: Integrated Verification for Agile Hardware Design. | Cristian Mattarei, Makai Mann, Clark W. Barrett, Ross G. Daly, Dillon Huff, Pat Hanrahan |
| 2018 | Template-Based Verification of Heap-Manipulating Programs. | Viktor Malk, Martin Hruska, Peter Schrammel, Toms Vojnar |
| 2018 | Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation. | Bjrnar Luteberget, Koen Claessen, Christian Johansen |
| 2018 | BMC with Memory Models as Modules. | Hernn Ponce de Len, Florian Furbach, Keijo Heljanko, Roland Meyer |
| 2018 | The FMCAD 2018 Graduate Student Forum. | Dejan Jovanovic, Andrew Reynolds |
| 2018 | k-FAIR = k-LIVENESS + FAIR Revisiting SAT-based Liveness Algorithms. | Alexander Ivrii, Ziv Nevo, Jason Baumgartner |
| 2018 | The ELDARICA Horn Solver. | Hossein Hojjat, Philipp Rmmer |
| 2018 | Certifying Proofs for LTL Model Checking. | Alberto Griggio, Marco Roveri, Stefano Tonetta |
| 2018 | Complete Test Sets And Their Approximations. | Eugene Goldberg |
| 2018 | Solving Constrained Horn Clauses Using Syntax and Data. | Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta |