Verification, Model Checking, and Abstract Interpretation: 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings | SpringerLink
Skip to main content
Springer Nature Link
Log in

Verification, Model Checking, and Abstract Interpretation

8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings

  • Conference proceedings
  • © 2007

Overview

Editors:
  1. Byron Cook
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Andreas Podelski
    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 4349)

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

Included in the following conference series:

Conference proceedings info: VMCAI 2007.

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

Access this book

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book JPY 7149
Price includes VAT (Japan)
  • 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

Keywords

Table of contents (27 papers)

  1. Front Matter

    Download chapter PDF

  2. Invited Talk

    1. DIVINE: DIscovering Variables IN Executables

      • Gogul Balakrishnan, Thomas Reps
      Pages 1-28

  3. Session 1

    1. Verifying Compensating Transactions

      • Michael Emmi, Rupak Majumdar
      Pages 29-43

    2. Model Checking Nonblocking MPI Programs

      • Stephen F. Siegel
      Pages 44-58

    3. Model Checking Via ΓCFA

      • Matthew Might, Benjamin Chambers, Olin Shivers
      Pages 59-73

    4. Using First-Order Theorem Provers in the Jahob Data Structure Verification System

      • Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin Rinard
      Pages 74-88

  4. Invited Tutorial

    1. Interpolants and Symbolic Model Checking

      • K. L. McMillan
      Pages 89-90

  5. Session 2

    1. Shape Analysis of Single-Parent Heaps

      • Ittai Balaban, Amir Pnueli, Lenore D. Zuck
      Pages 91-105

    2. An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures

      • Zvonimir Rakamarić, Jesse Bingham, Alan J. Hu
      Pages 106-121

    3. On Flat Programs with Lists

      • Marius Bozga, Radu Iosif
      Pages 122-136

  6. Invited Talk

    1. Automata-Theoretic Model Checking Revisited

      • Moshe Y. Vardi
      Pages 137-150

  7. Session 3

    1. Language-Based Abstraction Refinement for Hybrid System Verification

      • Felix Klaedtke, Stefan Ratschan, Zhikun She
      Pages 151-166

    2. More Precise Partition Abstractions

      • Harald Fecher, Michael Huth
      Pages 167-181

    3. The Spotlight Principle

      • Björn Wachter, Bernd Westphal
      Pages 182-198

    4. Lattice Automata

      • Orna Kupferman, Yoad Lustig
      Pages 199-213

  8. Invited Tutorial

    1. Learning Algorithms and Formal Verification (Invited Tutorial)

      • P. Madhusudan
      Pages 214-214

  9. Session 4

    1. Constructing Specialized Shape Analyses for Uniform Change

      • Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas Reps
      Pages 215-233

    2. Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning

      • Sigmund Cherem, Radu Rugina
      Pages 234-250

    3. Automated Verification of Shape and Size Properties Via Separation Logic

      • Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin
      Pages 251-266

  10. Invited Talk

    1. Towards Shape Analysis for Device Drivers

      • Hongseok Yang
      Pages 267-267
Back to top

Other volumes

  1. Verification, Model Checking, and Abstract Interpretation

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation