VMCAI 2019

27 papers

1. A Decidable Logic for Tree Data-Structures with Measurements · Xiaokang Qiu, Yanjun Wang
2. A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization · Richard Huybers, Alfons Laarman
3. A Practical Algorithm for Structure Embedding · Charlie Murphy, Zachary Kincaid
4. Application of Abstract Interpretation to the Automotive Electronic Control System · Tomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, Yoshiumi Kawamura
5. Automatic Program Repair Using Formal Verification and Expression Templates · Thanh-Toan Nguyen, Quang-Trung Ta, Wei-Ngan Chin
6. Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics · Stefan Haar, Juraj Kolcák, Loïc Paulevé
7. Demand Control-Flow Analysis · Kimball Germane, Jay McCarthy, Michael D. Adams, Matthew Might
8. Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis · Rémy Boutonnet, Nicolas Halbwachs
9. Effect-Driven Flow Analysis · Jens Nicolay, Quentin Stiévenart, Wolfgang De Meuter, Coen De Roover
10. Exploiting Pointer Analysis in Memory Models for Deductive Verification · Quentin Bouillaguet, François Bobot, Mihaela Sighireanu, Boris Yakobowski
11. Fast BGP Simulation of Large Datacenters · Nuno P. Lopes, Andrey Rybalchenko
12. Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic · Normann Decker, Anton Pirogov
13. Lazy but Effective Functional Synthesis · Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta
14. Mechanically Proving Determinacy of Hierarchical Block Diagram Translations · Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis
15. Minimal Synthesis of String to String Functions from Examples · Jad Hamza, Viktor Kuncak
16. On the Semantics of Snapshot Isolation · Azalea Raad, Ori Lahav, Viktor Vafeiadis
17. Parametric Timed Broadcast Protocols · Étienne André, Benoît Delahaye, Paulin Fournier, Didier Lime
18. Program Synthesis with Equivalence Reduction · Calvin Smith, Aws Albarghouthi
19. Relatively Complete Pushdown Analysis of Escape Continuations · Kimball Germane, Matthew Might
20. Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs · Anja F. Karl, Robert Schilling, Roderick Bloem, Stefan Mangard
21. Solving and Interpolating Constant Arrays Based on Weak Equivalences · Jochen Hoenicke, Tanja Schindler
22. Static Analysis of Binary Code with Memory Indirections Using Polyhedra · Clément Ballabriga, Julien Forget, Laure Gonnord, Giuseppe Lipari, Jordy Ruiz
23. Syntactic Partial Order Compression for Probabilistic Reachability · Gereon Fox, Daniel Stan, Holger Hermanns
24. Termination of Nondeterministic Probabilistic Programs · Hongfei Fu, Krishnendu Chatterjee
25. Type-Directed Bounding of Collections in Reactive Programs · Tianhan Lu, Pavol Cerný, Bor-Yuh Evan Chang, Ashutosh Trivedi
26. Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking · Étienne André, Laurent Fribourg, Jean-Marc Mota, Romain Soulat
27. euforia: Complete Software Model Checking with Uninterpreted Functions · Denis Bueno, Karem A. Sakallah