| 2020 | 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020 |
| 2020 | A Theoretical Framework for Symbolic Quick Error Detection. Florian Lonsing, Subhasish Mitra, Clark W. Barrett |
| 2020 | Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration. Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, Kristin Y. Rozier |
| 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 | Anytime Algorithms for MaxSAT and Beyond. Alexander Nadel |
| 2020 | Art: Abstraction Refinement-Guided Training for Provably Correct Neural Networks. Xuankang Lin, He Zhu, Roopsha Samanta, Suresh Jagannathan |
| 2020 | Automating Compositional Analysis of Authentication Protocols. Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, Corina S. Pasareanu |
| 2020 | Automating Modular Verification of Secure Information Flow. Lauren Pick, Grigory Fedyukovich, Aarti Gupta |
| 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 | Effective System Level Liveness Verification. Alexander Fedotov, Jeroen J. A. Keiren, Julien Schmaltz |
| 2020 | Formal Methods with a Touch of Magic. Parand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger, Anna Lukina |
| 2020 | Formal Verification for Natural and Engineered Biological Systems. Hillel Kugler |
| 2020 | From Correctness to High Quality. Orna Kupferman |
| 2020 | How testable is business software? Peter Schrammel |
| 2020 | Incremental Verification by SMT-based Summary Repair. Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina |
| 2020 | Learning Properties in LTL ∩ ACTL from Positive Examples Only. Rüdiger Ehlers, Ivan Gavran, Daniel Neider |
| 2020 | Model Checking Software-Defined Networks with Flow Entries that Time Out. Vasileios Klimis, George Parisis, Bernhard Reus |
| 2020 | On Optimizing a Generic Function in SAT. Alexander Nadel |
| 2020 | Parallelization Techniques for Verifying Neural Networks. Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett |
| 2020 | Reactive Synthesis from Extended Bounded Response LTL Specifications. Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta |
| 2020 | Reductions for Strings and Regular Expressions Revisited. Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli |
| 2020 | Runtime Verification on FPGAs with LTLf Specifications. Tommy Tracy II, Lucas M. Tabajara, Moshe Y. Vardi, Kevin Skadron |
| 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 | Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. Franz Brauße, Zurab Khasidashvili, Konstantin Korovin |
| 2020 | Smart Induction for Isabelle/HOL (Tool Paper). Yutaka Nagashima |
| 2020 | Switss: Computing Small Witnessing Subsystems. Simon Jantsch, Hans Harder, Florian Funke, Christel Baier |
| 2020 | Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. Aina Niemetz, Mathias Preiner |
| 2020 | The FMCAD 2020 Student Forum. Peter Schrammel |
| 2020 | The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. Daniela Kaufmann, Mathias Fleury, Armin Biere |
| 2020 | Thread-modular Counter Abstraction for Parameterized Program Safety. Thomas Pani, Georg Weissenbacher, Florian Zuleger |
| 2020 | Trace Logic for Inductive Loop Reasoning. Pamina Georgiou, Bernhard Gleiss, Laura Kovács |
| 2020 | Tutorial on World-Level Model Checking. Armin Biere |
| 2020 | Using model checking tools to triage the severity of security bugs in the Xen hypervisor. Byron Cook, Björn Döbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz |
| 2020 | Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning. Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, Jakob Nordström |