Verification, Model Checking, and Abstract Interpretation

1. Front Matter

   Pages i-xiv

   PDF

2. Witnessing Secure Compilation

   • Kedar S. Namjoshi, Lucas M. Tabajara

   Pages 1-22

3. \(\mathsf {BackFlow}\): Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results

   • Pietro Ferrara, Luca Olivieri, Fausto Spoto

   Pages 23-43

4. Fixing Code that Explodes Under Symbolic Evaluation

   • Sorawee Porncharoenwase, James Bornholt, Emina Torlak

   Pages 44-67

5. The Correctness of a Code Generator for a Functional Language

   • Nathanaël Courant, Antoine Séré, Natarajan Shankar

   Pages 68-89

6. Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification

   • Jack J. Garzella, Marek Baranowski, Shaobo He, Zvonimir Rakamarić

   Pages 90-111

7. Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction

   • Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham

   Pages 112-135

8. A Systematic Approach to Abstract Interpretation of Program Transformations

   • Sven Keidel, Sebastian Erdweg

   Pages 136-157

9. Sharing Ghost Variables in a Collection of Abstract Domains

   • Marc Chevalier, Jérôme Feret

   Pages 158-179

10. Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation

    • Oren Ish-Shalom, Shachar Itzhaky, Roman Manevich, Noam Rinetzky

    Pages 180-201

11. Synthesizing Environment Invariants for Modular Hardware Verification

    • Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik

    Pages 202-225

12. Systematic Classification of Attackers via Bounded Model Checking

    • Eric Rothstein-Morris, Jun Sun, Sudipta Chattopadhyay

    Pages 226-247

13. Cheap CTL Compassion in NuSMV

    • Daniel Hausmann, Tadeusz Litak, Christoph Rauch, Matthias Zinner

    Pages 248-269

14. A Cooperative Parallelization Approach for Property-Directed k-Induction

    • Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina

    Pages 270-292

15. Generalized Property-Directed Reachability for Hybrid Systems

    • Kohei Suenaga, Takuya Ishizawa

    Pages 293-313

16. Language Inclusion for Finite Prime Event Structures

    • Andreas Fellner, Thorsten Tarrach, Georg Weissenbacher

    Pages 314-336

17. Promptness and Bounded Fairness in Concurrent and Parameterized Systems

    • Swen Jacobs, Mouhammad Sakr, Martin Zimmermann

    Pages 337-359

18. Solving \(\mathrm {LIA} ^\star \) Using Approximations

    • Maxwell Levatich, Nikolaj Bjørner, Ruzica Piskac, Sharon Shoham

    Pages 360-378

19. Formalizing and Checking Multilevel Consistency

    • Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Gautham Shenoy R., S. P. Suresh

    Pages 379-400

20. Practical Abstractions for Automated Verification of Shared-Memory Concurrency

    • Wytse Oortwijn, Dilian Gurov, Marieke Huisman

    Pages 401-425

This book constitutes the proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020. The 21 papers presented in this volume were carefully reviewed from 44 submissions. VMCAI provides a forum for researchers from the communities of verification, model checking, and abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. 

• architecture verification and validation
• artificial intelligence
• computer programming
• computer systems
• distributed computer systems
• embedded systems
• engineering
• formal logic
• graph theory
• mathematics
• model checking
• parallel processing systems
• software architecture
• software design
• software engineering
• software quality
• theoretical computer science
• verification
• verification and validation
• data structures

• Ludwig-Maximilians-Universität München, Munich, Germany

  Dirk Beyer

• Max Planck Institute for Software Systems, Kaiserslautern, Germany

  Damien Zufferey

Policies and ethics