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

Invited Talk

Gogul Balakrishnan, Thomas W. Reps:
DIVINE: DIscovering Variables IN Executables. 1-28

Session 1

Michael Emmi, Rupak Majumdar:
Verifying Compensating Transactions. 29-43
Stephen F. Siegel:
Model Checking Nonblocking MPI Programs. 44-58
Matthew Might, Benjamin Chambers, Olin Shivers:
Model Checking Via GammaCFA. 59-73
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

Invited Tutorial

Kenneth L. McMillan:
Interpolants and Symbolic Model Checking. 89-90

Session 2

Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Shape Analysis of Single-Parent Heaps. 91-105
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
Marius Bozga, Radu Iosif:
On Flat Programs with Lists. 122-136

Invited Talk

Moshe Y. Vardi:
Automata-Theoretic Model Checking Revisited. 137-150

Session 3

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

Invited Tutorial

P. Madhusudan:
Learning Algorithms and Formal Verification (Invited Tutorial). 214

Session 4

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

Invited Talk

Hongseok Yang:
Towards Shape Analysis for Device Drivers. 267

Session 5

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

Invited Tutorial

Peter Z. Revesz:
The Constraint Database Approach to Software Verification. 329-345

Session 6

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