PROCEEDINGS OF THE 20TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2020

Contents

Tutorials
Anytime Algorithms for MaxSAT and Beyond
Alexander Nadel

Formal Verification for Natural and Engineered Biological Systems
Hillel Kugler

Tutorial on World-Level Model Checking
Armin Biere

Invited Talks
How testable is business software?
Peter Schrammel

From Correctness to High Quality
Orna Kupferman

Student Forum
The FMCAD 2020 Student Forum
Peter Schrammel

Hardware Verification
Effective System Level Liveness Verification
Alexander Fedotov, Jeroen J.A. Keiren and Julien Schmaltz

Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams and Kristin Yvonne Rozier

A Theoretical Framework for Symbolic Quick Error Detection
Florian Lonsing, Subhasish Mitra and Clark Barrett

Runtime Verification on FPGAs with LTLf Specifications
Tommy Tracy II, Lucas Tabajara, Moshe Vardi and Kevin Skadron

Software Verification
Distributed Bounded Model Checking
Prantik Chatterjee, Subhajit Roy, Bui Phi Diep and Akash Lal

EUFicient Reachability for Software with Arrays
Denis Bueno, Arlen Cox and Karem A. Sakallah

Thread-modular Counter Abstraction for Parameterized Program Safety
Thomas Pani, Georg Weissenbacher and Florian Zuleger

Incremental Verification by SMT-based Summary Repair
Sepideh Asadi, Martin Blicha, Antti Hyv¨arinen, Grigory Fedyukovich and Natasha Sharygina

Software Verification and Learning
Reactive Synthesis from Extended Bounded Response LTL Specifications
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari and Stefano Tonetta

SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury and Cesare Tinelli

Learning Properties in LTL ∩ ACTL from Positive Examples Only
Rüdiger Ehlers, Ivan Gavran and Daniel Neider

Automating Compositional Analysis of Authentication Protocols
Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia and Corina Pasareanu

Verification and Neural Networks
Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation
Franz Brauße, Zurab Khasidashvili and Konstantin Korovin

Parallelization Techniques for Verifying Neural Networks
Haoze Wu, Alex Ozdemir, Aleksandar Zelji´c, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu and Clark Barrett

Formal Methods with a Touch of Magic
Parand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger and Anna Lukina

ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Xuankang Lin, He Zhu, Roopsha Samanta and Suresh Jagannathan

Applied Verification
Automating Modular Verification of Secure Information Flow
Lauren Pick, Grigory Fedyukovich and Aarti Gupta

Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg and Chetan Bansal

Model Checking Software-Defined Networks with Flow Entries that Time Out
Vasileios Klimis, George Parisis and Bernhard Reus

Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Byron Cook, Bjoern Doebel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig and Pawel Wieczorkiewicz

SAT / SMT
Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers and Jakob Nordstrom

On Optimizing a Generic Function in SAT
Alexander Nadel

Ternary Propagation-Based Local Search for More Bit-Precise Reasoning
Aina Niemetz and Mathias Preiner

Reductions for Strings and Regular Expressions Revisited
Andrew Reynolds, Andres Noetzli, Clark Barrett and Cesare Tinelli

Theory and Theorem Proving
SWITSS: Computing Small Witnessing Subsystems
Simon Jantsch, Hans Harder, Florian Funke and Christel Baier

Smart Induction for Isabelle/HOL (Tool Paper)
Yutaka Nagashima

Trace Logic for Inductive Loop Reasoning
Pamina Georgiou, Bernhard Gleiss and Laura Kovacs

The Proof Checkers Pacheck and Past`eque for the Practical Algebraic Calculus
Daniela Kaufmann, Mathias Fleury and Armin Biere