Skip to main content
SpringerLink
Log in
Book cover

Verification, Model Checking, and Abstract Interpretation

18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings

  • Conference proceedings
  • © 2017

Overview

Editors:
  1. Ahmed Bouajjani

    1. IRIF, Université Paris Diderot, Paris, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. David Monniaux

    1. VERIMAG, CNRS & Université Grenoble Alpes, Grenoble, France

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

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

Included in the following conference series:

Conference proceedings info: VMCAI 2017.

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 (29 papers)

  1. Front Matter

    Pages I-XVII
    Download chapter PDF

  2. Bringing LTL Model Checking to Biologists

    • Zara Ahmed, David Benque, Sergey Berezin, Anna Caroline E. Dahl, Jasmin Fisher, Benjamin A. Hall et al.
    Pages 1-13

  3. Detecting Strict Aliasing Violations in the Wild

    • Pascal Cuoq, Loïc Runarvot, Alexander Cherepanov
    Pages 14-33

  4. Effective Bug Finding in C Programs with Shape and Effect Abstractions

    • Iago Abal, Claus Brabrand, Andrzej Wąsowski
    Pages 34-54

  5. Synthesizing Non-Vacuous Systems

    • Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman
    Pages 55-72

  6. Static Analysis of Communicating Processes Using Symbolic Transducers

    • Vincent Botbol, Emmanuel Chailloux, Tristan Le Gall
    Pages 73-90

  7. Reduction of Workflow Nets for Generalised Soundness Verification

    • Hadrien Bride, Olga Kouchnarenko, Fabien Peureux
    Pages 91-111

  8. Structuring Abstract Interpreters Through State and Value Abstractions

    • Sandrine Blazy, David Bühler, Boris Yakobowski
    Pages 112-130

  9. Matching Multiplications in Bit-Vector Formulas

    • Supratik Chakraborty, Ashutosh Gupta, Rahul Jain
    Pages 131-150

  10. Independence Abstractions and Models of Concurrency

    • Vijay D’Silva, Daniel Kroening, Marcelo Sousa
    Pages 151-168

  11. Complete Abstractions and Subclassical Modal Logics

    • Vijay D’Silva, Marcelo Sousa
    Pages 169-186

  12. Using Abstract Interpretation to Correct Synchronization Faults

    • Pietro Ferrara, Omer Tripp, Peng Liu, Eric Koskinen
    Pages 187-208

  13. Property Directed Reachability for Proving Absence of Concurrent Modification Errors

    • Asya Frumkin, Yotam M. Y. Feldman, Ondřej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham
    Pages 209-227

  14. Stabilizing Floating-Point Programs Using Provenance Analysis

    • Yijia Gu, Thomas Wahl
    Pages 228-245

  15. Dynamic Reductions for Model Checking Concurrent Software

    • Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher
    Pages 246-265

  16. Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

    • Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang
    Pages 266-287

  17. Counterexample Validation and Interpolation-Based Refinement for Forest Automata

    • Lukáš Holík, Martin Hruška, Ondřej Lengál, Adam Rogalewicz, Tomáš Vojnar
    Pages 288-309

  18. Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT

    • Jiahong Jiang, Liqian Chen, Xueguang Wu, Ji Wang
    Pages 310-329

  19. Solving Nonlinear Integer Arithmetic with MCSAT

    • Dejan Jovanović
    Pages 330-346

  20. Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

    • Igor Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi
    Pages 347-366
Back to top

Other volumes

  1. Verification, Model Checking, and Abstract Interpretation

Keywords

About this book

This book constitutes the refereed proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, held in Paris, France, in January 2017.

The 27 full papers together with 3 invited keynotes presented were carefully reviewed and selected from 60 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type systems, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems.

 

Editors and Affiliations

  • IRIF, Université Paris Diderot, Paris, France

    Ahmed Bouajjani

  • VERIMAG, CNRS & Université Grenoble Alpes, Grenoble, France

    David Monniaux

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation