Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2020

Table of Contents: Anytime Algorithms for MaxSAT and Beyond / by Alexander Nadel (p. 1) -- Formal Verification for Natural and Engineered Biological Systems / by Hillel Kugler (p. 2) -- Tutorial on World-Level Model Checking / by Armin Biere (p. 3) -- How Testable is Business Software? / by Peter Schrammel (p. 4) -- From Correctness to High Quality / by Orna Kupferman (p. 5) -- The FMCAD 2020 Student Forum / Peter Schrammel (p. 6) -- Effective System Level Liveness Verification / by Alexander Fedotov, Jeroen J.A. Keiren, and Julien Schmaltz (p. 7) -- Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration / by Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, and Kristin Yvonne Rozier (p. 16) -- A Theoretical Framework for Symbolic Quick Error Detection / by Florian Lonsing, Subhasish Mitra, and Clark Barrett (p. 26) -- Runtime Verification on FPGAs and LTLf Specifications / by Tommy Tracy II, Lucas Tabajara, Moshe Vardi, and Kevin Skadron (p. 36) -- Distributed Bounded Model Checking / by Prantik Chatterjee, Subhajit Roy, Bui Phi Diep, and Akash Lal (p. 47) -- EUFicient Reachability for Software with Arrays / by Denis Bueno, Arlen Cox, and Karem A. Sakallah (p. 57) -- Thread-modular Counter Abstraction for Parameterized Program Safety / by Thomas Pani, Georg Weissenbacher, and Florian Zuleger (p. 67) -- Incremental Verification by SMT-based Summary Repair / by Sepideh Asadi, Martin Blicha, Antti Hyvärinen, Grigory Fedyukovich, and Natasha Sharygina (p. 77) -- Reactive Synthesis from Extended Bounded Response LTL Specifications / by Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, and Stefano Tonetta (p. 83) -- SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces / by M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, and Cesare Tinelli (p. 93) -- Learning Properties in LTL ∩ ACTL from Positive Examples Only / by Rüdiger Ehlers, Ivan Gavran, and Daniel Neider (p. 104) -- Automating Compositional Analysis of Authentication Protocols / by Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, and Corina Pasareanu (p. 113) -- Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation / by Franz Brauße, Zurab Khasidashvili, and Konstantin Korovin (p. 119) -- Parallelization Techniques for Verifying Neural Networks / by Haoze Wu, Alex Ozdemir, Aleksandar Zeljić, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, and Clark Barrett (p. 128) -- Formal Methods with a Touch of Magic / by Parand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger, and Anna Lukina (p. 138) -- ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks / by Xuankang Lin, He Zhu, Roopsha Samanta, and Suresh Jagannathan (p. 148) -- Automating Modular Verification of Secure Information Flow / by Lauren Pick, Grigory Fedyukovich, and Aarti Gupta (p. 158) -- Angelic Checking within Static Driver Verifier: Towards High-precision Defects without (modeling) Cost / by Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, and Chetan Bansal (p. 169) -- Model Checking Software-Defined Networks with Flow Entries that Time Out / by Vasileios Klimis, George Parisis, and Bernhard Reus (p. 179) -- Using Model Checking Tools to Triage the Severity of Security Bugs in the Xen Hypervisor / by Byron Cook, Bjoern Doebel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, and Pawel Wieczorkiewicz (p. 185) -- Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning / by Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, and Jakob Nordstrom (p. 194) -- On Optimizing a Generic Function in SAT / by Alexander Nadel (p. 205) -- Ternary Propagation-Based Local Search for More Bit-Precise Reasoning / by Aina Niemetz, and Mathias Preiner (p. 214) -- Reductions for Strings and Regular Expressions Revisited / by Andrew Reynolds, Andres Noetzli, Clark Barrett, and Cesare Tinelli (p. 225) -- SWITSS: Computing Small Witnessing Subsystems / by Simon Jantsch, Hans Harder, Florian Funke, and Christel Baier (p. 236) -- Smart Induction for Isabelle/HOL (Tool Paper) / by Yutaka Nagashima (p. 245) -- Trace Logic for Inductive Loop Reasoning / by Pamina Georgiou, Bernhard Gleiss, and Laura Kovacs (p. 255) -- The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus / by Daniela Kaufmann, Mathias Fleury, and Armin Biere (p. 264)