8. VMCAI 2007: Nice, France

Byron Cook, Andreas Podelski (Eds.): Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings. Lecture Notes in Computer Science 4349 Springer 2007, ISBN 978-3-540-69735-0 BibTeX

Invited Talk

Gogul Balakrishnan, Thomas W. Reps:
DIVINE: DIscovering Variables IN Executables. 1-28
Electronic Edition (link) BibTeX

Session 1

Michael Emmi, Rupak Majumdar:
Verifying Compensating Transactions. 29-43
Electronic Edition (link) BibTeX
Stephen F. Siegel:
Model Checking Nonblocking MPI Programs. 44-58
Electronic Edition (link) BibTeX
Matthew Might, Benjamin Chambers, Olin Shivers:
Model Checking Via GammaCFA. 59-73
Electronic Edition (link) BibTeX
Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin C. Rinard:
Using First-Order Theorem Provers in the Jahob Data Structure Verification System. 74-88
Electronic Edition (link) BibTeX

Invited Tutorial

Kenneth L. McMillan:
Interpolants and Symbolic Model Checking. 89-90
Electronic Edition (link) BibTeX

Session 2

Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Shape Analysis of Single-Parent Heaps. 91-105
Electronic Edition (link) BibTeX
Zvonimir Rakamaric, Jesse D. Bingham, Alan J. Hu:
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures. 106-121
Electronic Edition (link) BibTeX
Marius Bozga, Radu Iosif:
On Flat Programs with Lists. 122-136
Electronic Edition (link) BibTeX

Invited Talk

Moshe Y. Vardi:
Automata-Theoretic Model Checking Revisited. 137-150
Electronic Edition (link) BibTeX

Session 3

Felix Klaedtke, Stefan Ratschan, Zhikun She:
Language-Based Abstraction Refinement for Hybrid System Verification. 151-166
Electronic Edition (link) BibTeX
Harald Fecher, Michael Huth:
More Precise Partition Abstractions. 167-181
Electronic Edition (link) BibTeX
Björn Wachter, Bernd Westphal:
The Spotlight Principle. 182-198
Electronic Edition (link) BibTeX
Orna Kupferman, Yoad Lustig:
Lattice Automata. 199-213
Electronic Edition (link) BibTeX

Invited Tutorial

P. Madhusudan:
Learning Algorithms and Formal Verification (Invited Tutorial). 214
Electronic Edition (link) BibTeX

Session 4

Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps:
Constructing Specialized Shape Analyses for Uniform Change. 215-233
Electronic Edition (link) BibTeX
Sigmund Cherem, Radu Rugina:
Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning. 234-250
Electronic Edition (link) BibTeX
Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin:
Automated Verification of Shape and Size Properties Via Separation Logic. 251-266
Electronic Edition (link) BibTeX

Invited Talk

Hongseok Yang:
Towards Shape Analysis for Device Drivers. 267
Electronic Edition (link) BibTeX

Session 5

Mathias Péron, Nicolas Halbwachs:
An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints. 268-282
Electronic Edition (link) BibTeX
Francesco Logozzo:
Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes. 283-298
Electronic Edition (link) BibTeX
Kedar S. Namjoshi:
Symmetry and Completeness in the Analysis of Parameterized Systems. 299-313
Electronic Edition (link) BibTeX
Thomas Ball, Orna Kupferman:
Better Under-Approximation of Programs by Hiding Variables. 314-328
Electronic Edition (link) BibTeX

Invited Tutorial

Peter Z. Revesz:
The Constraint Database Approach to Software Verification. 329-345
Electronic Edition (link) BibTeX

Session 6

Andrey Rybalchenko, Viorica Sofronie-Stokkermans:
Constraint Solving for Interpolation. 346-362
Electronic Edition (link) BibTeX
Sumit Gulwani, Ashish Tiwari:
Assertion Checking Unified. 363-377
Electronic Edition (link) BibTeX
Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko:
Invariant Synthesis for Combined Theories. 378-394
Electronic Edition (link) BibTeX