Verification, Model Checking, and Abstract Interpretation: 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings (Lecture Notes in Computer Science, 10747)

This book constitutes the refereed proceedings of the 19th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2018, held in Los Angeles, CA, USA, in January 2018. The 24 full papers presented together with the abstracts of 3 invited keynotes and 1 invited tutorial were carefully reviewed and selected from 43 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-XVIII Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction (Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger)....Pages 1-24 Gradual Program Verification (Johannes Bader, Jonathan Aldrich, Éric Tanter)....Pages 25-46 Automatic Verification of RMA Programs via Abstraction Extrapolation (Cedric Baumann, Andrei Marian Dan, Yuri Meshman, Torsten Hoefler, Martin Vechev)....Pages 47-70 Scalable Approximation of Quantitative Information Flow in Programs (Fabrizio Biondi, Michael A. Enescu, Annelie Heuser, Axel Legay, Kuldeep S. Meel, Jean Quilbeuf)....Pages 71-93 Code Obfuscation Against Abstract Model Checking Attacks (Roberto Bruni, Roberto Giacobazzi, Roberta Gori)....Pages 94-115 Abstract Code Injection (Samuele Buro, Isabella Mastroeni)....Pages 116-137 A Framework for Computer-Aided Design of Educational Domain Models (Eric Butler, Emina Torlak, Zoran Popović)....Pages 138-160 Automatic Verification of Intermittent Systems (Manjeet Dahiya, Sorav Bansal)....Pages 161-182 On abstraction and compositionality for weak-memory linearisability (Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong)....Pages 183-204 From Shapes to Amortized Complexity (Tomáš Fiedor, Lukáš Holík, Adam Rogalewicz, Moritz Sinn, Tomáš Vojnar, Florian Zuleger)....Pages 205-225 Invariant Generation for Multi-Path Loops with Polynomial Assignments (Andreas Humenberger, Maximilian Jaroschek, Laura Kovács)....Pages 226-246 Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity (Swen Jacobs, Mouhammad Sakr)....Pages 247-268 Refinement Types for Ruby (Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak)....Pages 269-290 Modular Analysis of Executables Using On-Demand Heyting Completion (Julian Kranz, Axel Simon)....Pages 291-312 Learning to Complement Büchi Automata (Yong Li, Andrea Turrini, Lijun Zhang, Sven Schewe)....Pages 313-335 \(P^5\): Planner-less Proofs of Probabilistic Parameterized Protocols (Lenore D. Zuck, Kenneth L. McMillan, Jordan Torf)....Pages 336-357 Co-Design and Verification of an Available File System (Mahsa Najafzadeh, Marc Shapiro, Patrick Eugster)....Pages 358-381 Abstraction-Based Interaction Model for Synthesis (Hila Peleg, Shachar Itzhaky, Sharon Shoham)....Pages 382-405 Generating Tests by Example (Hila Peleg, Dan Rasin, Eran Yahav)....Pages 406-429 A Logical System for Modular Information Flow Verification (Adi Prabawa, Mahmudul Faisal Al Ameen, Benedict Lee, Wei-Ngan Chin)....Pages 430-451 On Constructivity of Galois Connections (Francesco Ranzato)....Pages 452-473 Revisiting MITL to Fix Decision Procedures (Nima Roohi, Mahesh Viswanathan)....Pages 474-494 Selfless Interpolation for Infinite-State Model Checking (Tanja Schindler, Dejan Jovanović)....Pages 495-515 An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs (Laura Titolo, Marco A. Feliú, Mariano Moscato, César A. Muñoz)....Pages 516-537 Back Matter ....Pages 539-540