Skip to main content
SpringerLink
Log in
Book cover

Verification, Model Checking, and Abstract Interpretation

21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020, Proceedings

  • Conference proceedings
  • © 2020

Overview

Editors:
  1. Dirk Beyer

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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Damien Zufferey

    1. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 11990)

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Included in the following conference series:

Conference proceedings info: VMCAI 2020.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (21 papers)

  1. Front Matter

    Pages i-xiv
    Download chapter 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
Back to top

Other volumes

  1. Verification, Model Checking, and Abstract Interpretation

Keywords

About this book

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. 

Editors and Affiliations

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

    Dirk Beyer

  • Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Damien Zufferey

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation