Skip to main content
SpringerLink
Log in
Book cover

Verification, Model Checking, and Abstract Interpretation

20th International Conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019, Proceedings

  • Conference proceedings
  • © 2019

Overview

Editors:
  1. Constantin Enea

    1. IRIF, University Paris Diderot and CNRS, Paris, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Ruzica Piskac

    1. Yale University, New Haven, USA

    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 11388)

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

Included in the following conference series:

Conference proceedings info: VMCAI 2019.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.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 (27 papers)

  1. Front Matter

    Pages I-XVII
    Download chapter PDF

  2. On the Semantics of Snapshot Isolation

    • Azalea Raad, Ori Lahav, Viktor Vafeiadis
    Pages 1-23

  3. Program Synthesis with Equivalence Reduction

    • Calvin Smith, Aws Albarghouthi
    Pages 24-47

  4. Minimal Synthesis of String to String Functions from Examples

    • Jad Hamza, Viktor Kunčak
    Pages 48-69

  5. Automatic Program Repair Using Formal Verification and Expression Templates

    • Thanh-Toan Nguyen, Quang-Trung Ta, Wei-Ngan Chin
    Pages 70-91

  6. Lazy but Effective Functional Synthesis

    • Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta
    Pages 92-113

  7. Static Analysis of Binary Code with Memory Indirections Using Polyhedra

    • Clément Ballabriga, Julien Forget, Laure Gonnord, Giuseppe Lipari, Jordy Ruiz
    Pages 114-135

  8. Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis

    • Rémy Boutonnet, Nicolas Halbwachs
    Pages 136-159

  9. Exploiting Pointer Analysis in Memory Models for Deductive Verification

    • Quentin Bouillaguet, François Bobot, Mihaela Sighireanu, Boris Yakobowski
    Pages 160-182

  10. 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

  11. Relatively Complete Pushdown Analysis of Escape Continuations

    • Kimball Germane, Matthew Might
    Pages 205-225

  12. Demand Control-Flow Analysis

    • Kimball Germane, Jay McCarthy, Michael D. Adams, Matthew Might
    Pages 226-246

  13. Effect-Driven Flow Analysis

    • Jens Nicolay, Quentin Stiévenart, Wolfgang De Meuter, Coen De Roover
    Pages 247-274

  14. Type-Directed Bounding of Collections in Reactive Programs

    • Tianhan Lu, Pavol Černý, Bor-Yuh Evan Chang, Ashutosh Trivedi
    Pages 275-296

  15. Solving and Interpolating Constant Arrays Based on Weak Equivalences

    • Jochen Hoenicke, Tanja Schindler
    Pages 297-317

  16. A Decidable Logic for Tree Data-Structures with Measurements

    • Xiaokang Qiu, Yanjun Wang
    Pages 318-341

  17. A Practical Algorithm for Structure Embedding

    • Charlie Murphy, Zachary Kincaid
    Pages 342-362

  18. euforia: Complete Software Model Checking with Uninterpreted Functions

    • Denis Bueno, Karem A. Sakallah
    Pages 363-385

  19. Fast BGP Simulation of Large Datacenters

    • Nuno P. Lopes, Andrey Rybalchenko
    Pages 386-408

  20. 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
Back to top

Other volumes

  1. Verification, Model Checking, and Abstract Interpretation

Keywords

About this book

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.

Editors and Affiliations

  • IRIF, University Paris Diderot and CNRS, Paris, France

    Constantin Enea

  • Yale University, New Haven, USA

    Ruzica Piskac

Bibliographic Information

  • Book Title: Verification, Model Checking, and Abstract Interpretation

  • Book Subtitle: 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019, Proceedings

  • Editors: Constantin Enea, Ruzica Piskac

  • Series Title: Lecture Notes in Computer Science

  • DOI: https://doi.org/10.1007/978-3-030-11245-5

  • Publisher: Springer Cham

  • eBook Packages: Computer Science, Computer Science (R0)

  • Copyright Information: Springer Nature Switzerland AG 2019

  • Softcover ISBN: 978-3-030-11244-8Published: 11 January 2019

  • eBook ISBN: 978-3-030-11245-5Published: 10 January 2019

  • Series ISSN: 0302-9743

  • Series E-ISSN: 1611-3349

  • Edition Number: 1

  • Number of Pages: XVII, 602

  • Number of Illustrations: 1260 b/w illustrations, 69 illustrations in colour

  • Topics: Logics and Meanings of Programs, Software Engineering, Computer Communication Networks

Publish with us

Policies and ethics

Back to top

Search

Navigation