| 2020 | On Optimizing a Generic Function in SAT. | Alexander Nadel |
| 2020 | Anytime Algorithms for MaxSAT and Beyond. | Alexander Nadel |
| 2020 | A Theoretical Framework for Symbolic Quick Error Detection. | Florian Lonsing, Subhasish Mitra, Clark W. Barrett |
| 2020 | Art: Abstraction Refinement-Guided Training for Provably Correct Neural Networks. | Xuankang Lin, He Zhu, Roopsha Samanta, Suresh Jagannathan |
| 2020 | Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning. | Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, Jakob Nordstrm |
| 2020 | Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. | Shuvendu K. Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal |
| 2020 | From Correctness to High Quality. | Orna Kupferman |
| 2020 | Formal Verification for Natural and Engineered Biological Systems. | Hillel Kugler |
| 2020 | Model Checking Software-Defined Networks with Flow Entries that Time Out. | Vasileios Klimis, George Parisis, Bernhard Reus |
| 2020 | The Proof Checkers Pacheck and Pastque for the Practical Algebraic Calculus. | Daniela Kaufmann, Mathias Fleury, Armin Biere |
| 2020 | Switss: Computing Small Witnessing Subsystems. | Simon Jantsch, Hans Harder, Florian Funke, Christel Baier |
| 2020 | Trace Logic for Inductive Loop Reasoning. | Pamina Georgiou, Bernhard Gleiss, Laura Kovcs |
| 2020 | Effective System Level Liveness Verification. | Alexander Fedotov, Jeroen J. A. Keiren, Julien Schmaltz |
| 2020 | Learning Properties in LTL ∩ ACTL from Positive Examples Only. | Rdiger Ehlers, Ivan Gavran, Daniel Neider |
| 2020 | Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration. | Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, Kristin Y. Rozier |
| 2020 | Using model checking tools to triage the severity of security bugs in the Xen hypervisor. | Byron Cook, Bjrn Dbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz |
| 2020 | Reactive Synthesis from Extended Bounded Response LTL Specifications. | Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta |
| 2020 | Distributed Bounded Model Checking. | Prantik Chatterjee, Subhajit Roy, Bui Phi Diep, Akash Lal |
| 2020 | EUFicient Reachability in Software with Arrays. | Denis Bueno, Arlen Cox, Karem A. Sakallah |
| 2020 | Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. | Franz Braue, Zurab Khasidashvili, Konstantin Korovin |
| 2020 | Tutorial on World-Level Model Checking. | Armin Biere |
| 2020 | Incremental Verification by SMT-based Summary Repair. | Sepideh Asadi, Martin Blicha, Antti E. J. Hyvrinen, Grigory Fedyukovich, Natasha Sharygina |
| 2020 | SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. | M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli |
| 2020 | Formal Methods with a Touch of Magic. | Parand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger, Anna Lukina |
| 2019 | Challenges and Solutions in Post-Silicon Validation of High-end Processors (Invited Tutorial). | Avi Ziv |