Accepted Papers

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