Verification, Model Checking, and Abstract Interpretation: 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019, Proceedings (Lecture Notes in Computer Science, 11388)

This book constitutes the refereed proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2019, held in Cascais, Portugal, in January 2019. The 27 full papers presented together with the abstracts of 3 invited keynote talks were carefully reviewed and selected from 62 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation, program synthesis, static analysis, type systems, deductive methods, program certification, decision procedures, theorem proving, program certification, debugging techniques, program transformation, optimization, and hybrid and cyber-physical systems. Front Matter ....Pages I-XVII On the Semantics of Snapshot Isolation (Azalea Raad, Ori Lahav, Viktor Vafeiadis)....Pages 1-23 Program Synthesis with Equivalence Reduction (Calvin Smith, Aws Albarghouthi)....Pages 24-47 Minimal Synthesis of String to String Functions from Examples (Jad Hamza, Viktor Kunčak)....Pages 48-69 Automatic Program Repair Using Formal Verification and Expression Templates (Thanh-Toan Nguyen, Quang-Trung Ta, Wei-Ngan Chin)....Pages 70-91 Lazy but Effective Functional Synthesis (Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta)....Pages 92-113 Static Analysis of Binary Code with Memory Indirections Using Polyhedra (Clément Ballabriga, Julien Forget, Laure Gonnord, Giuseppe Lipari, Jordy Ruiz)....Pages 114-135 Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis (Rémy Boutonnet, Nicolas Halbwachs)....Pages 136-159 Exploiting Pointer Analysis in Memory Models for Deductive Verification (Quentin Bouillaguet, François Bobot, Mihaela Sighireanu, Boris Yakobowski)....Pages 160-182 Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs (Anja F. Karl, Robert Schilling, Roderick Bloem, Stefan Mangard)....Pages 183-204 Relatively Complete Pushdown Analysis of Escape Continuations (Kimball Germane, Matthew Might)....Pages 205-225 Demand Control-Flow Analysis (Kimball Germane, Jay McCarthy, Michael D. Adams, Matthew Might)....Pages 226-246 Effect-Driven Flow Analysis (Jens Nicolay, Quentin Stiévenart, Wolfgang De Meuter, Coen De Roover)....Pages 247-274 Type-Directed Bounding of Collections in Reactive Programs (Tianhan Lu, Pavol Černý, Bor-Yuh Evan Chang, Ashutosh Trivedi)....Pages 275-296 Solving and Interpolating Constant Arrays Based on Weak Equivalences (Jochen Hoenicke, Tanja Schindler)....Pages 297-317 A Decidable Logic for Tree Data-Structures with Measurements (Xiaokang Qiu, Yanjun Wang)....Pages 318-341 A Practical Algorithm for Structure Embedding (Charlie Murphy, Zachary Kincaid)....Pages 342-362 euforia: Complete Software Model Checking with Uninterpreted Functions (Denis Bueno, Karem A. Sakallah)....Pages 363-385 Fast BGP Simulation of Large Datacenters (Nuno P. Lopes, Andrey Rybalchenko)....Pages 386-408 Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking (Étienne André, Laurent Fribourg, Jean-Marc Mota, Romain Soulat)....Pages 409-424 Application of Abstract Interpretation to the Automotive Electronic Control System (Tomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, Yoshiumi Kawamura)....Pages 425-445 Syntactic Partial Order Compression for Probabilistic Reachability (Gereon Fox, Daniel Stan, Holger Hermanns)....Pages 446-467 Termination of Nondeterministic Probabilistic Programs (Hongfei Fu, Krishnendu Chatterjee)....Pages 468-490 Parametric Timed Broadcast Protocols (Étienne André, Benoit Delahaye, Paulin Fournier, Didier Lime)....Pages 491-512 Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic (Normann Decker, Anton Pirogov)....Pages 513-534 A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization (Richard Huybers, Alfons Laarman)....Pages 535-554 Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics (Stefan Haar, Juraj Kolčák, Loïc Paulevé)....Pages 555-576 Mechanically Proving Determinacy of Hierarchical Block Diagram Translations (Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis)....Pages 577-600 Back Matter ....Pages 601-602