Skip to main content
SpringerLink
Log in
Book cover

Verification, Model Checking, and Abstract Interpretation

10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings

  • Conference proceedings
  • © 2009

Overview

Editors:
  1. Neil D. Jones

    1. (Emeritus University of Copenhagen), Rungsted, Denmark

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Markus Müller-Olm

    1. Institut für Informatik, Fachbereich Mathematik und Informatik, Westfälische Wilhelms-Universität, Münster, 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 5403)

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

Included in the following conference series:

Conference proceedings info: VMCAI 2009.

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

    Download chapter PDF

  2. Invited Talks

    1. Model Checking: Progress and Problems

      • E. Allen Emerson
      Pages 1-1

    2. Model Checking Concurrent Programs

      • Aarti Gupta
      Pages 2-2

    3. Thread-Modular Shape Analysis

      • Mooly Sagiv
      Pages 3-3

  3. Invited Tutorials

    1. Advances in Program Termination and Liveness

      • Byron Cook
      Pages 4-4

    2. Verification of Security Protocols

      • Véronique Cortier
      Pages 5-13

  4. Submitted Papers

    1. Towards Automatic Stability Analysis for Rely-Guarantee Proofs

      • Hasan Amjad, Richard Bornat
      Pages 14-28

    2. Mostly-Functional Behavior in Java Programs

      • William C. Benton, Charles N. Fischer
      Pages 29-43

    3. The Higher-Order Aggregate Update Problem

      • Christos Dimoulas, Mitchell Wand
      Pages 44-58

    4. An Abort-Aware Model of Transactional Programming

      • Kousha Etessami, Patrice Godefroid
      Pages 59-73

    5. Model-Checking the Linux Virtual File System

      • Andy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg, Radu I. Siminiceanu
      Pages 74-88

    6. LTL Generalized Model Checking Revisited

      • Patrice Godefroid, Nir Piterman
      Pages 89-104

    7. Monitoring the Full Range of ω-Regular Properties of Stochastic Systems

      • Kalpana Gondi, Yogeshkumar Patel, A. Prasad Sistla
      Pages 105-119

    8. Constraint-Based Invariant Inference over Predicate Abstraction

      • Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan
      Pages 120-135

    9. Reducing Behavioural to Structural Properties of Programs with Procedures

      • Dilian Gurov, Marieke Huisman
      Pages 136-150

    10. Query-Driven Program Testing

      • Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
      Pages 151-166

    11. Average-Price-per-Reward Games on Hybrid Automata with Strong Resets

      • Marcin Jurdziński, Ranko Lazić, Michał Rutkowski
      Pages 167-181

    12. Abstraction Refinement for Probabilistic Software

      • Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, David Parker
      Pages 182-197

    13. Finding Concurrency-Related Bugs Using Random Isolation

      • Nicholas Kidd, Thomas Reps, Julian Dolby, Mandana Vaziri
      Pages 198-213

    14. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries

      • Johannes Kinder, Florian Zuleger, Helmut Veith
      Pages 214-228
Back to top

Other volumes

  1. Verification, Model Checking, and Abstract Interpretation

Keywords

About this book

This volume contains the proceedings of the 10th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2009), held in Savannah, Georgia, USA, January 18–20, 2009. VMCAI 2009 was the 10th in a series of meetings. Previous meetings were heldinPortJe?erson1997,Pisa1998,Venice2002,NewYork2003,Venice2004, Paris 2005, Charleston 2006, Nice 2007, and San Francisco 2008. VMCAI centers on state-of-the-art research relevant to analysis of programs and systems and drawn from three research communities: veri?cation, model checking, and abstract interpretation. A goal is to facilitate interaction, cro- fertilization, and the advance of hybrid methods that combine two or all three areas. Topics covered by VMCAI include program veri?cation, program cert- cation, model checking, debugging techniques, abstract interpretation, abstract domains, static analysis, type systems, deductive methods, and optimization. The Program Committee selected 24 papers out of 72 submissions based on anonymous reviews and discussions in an electronic Program Committee me- ing. The principal selection criteria were relevance and quality. VMCAI has a tradition of inviting distinguished speakers to give talks and tutorials. This time the program included three invited talks by: – E. Allen Emerson (University of Texas at Austin) on “Model Checking: Progress and Problems” – Aarti Gupta (NEC Labs, Princeton) on “Model Checking Concurrent Programs” – Mooly Sagiv (Tel-Aviv University) on “Thread Modular Shape Analysis” There were also two invited tutorials by: – Byron Cook (Microsoft Research, Cambridge) on “Proving Program Ter- nation and Liveness” – V´ eroniqueCortier (LORIA, CNRS, Nancy) on“Veri?cationof Security P- tocols”.

Editors and Affiliations

  • (Emeritus University of Copenhagen), Rungsted, Denmark

    Neil D. Jones

  • Institut für Informatik, Fachbereich Mathematik und Informatik, Westfälische Wilhelms-Universität, Münster, Germany

    Markus Müller-Olm

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation