6. VMCAI 2005: Paris, France

Radhia Cousot (Ed.): Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings. Lecture Notes in Computer Science 3385 Springer 2005, ISBN 3-540-24297-X

Invited Paper

Patrick Cousot:
Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. 1-24

Numerical Abstraction

Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna:
Scalable Analysis of Linear Systems Using Mathematical Programming. 25-41
Jérôme Feret:
The Arithmetic-Geometric Progression Abstract Domain. 42-58
Matthieu Martel:
An Overview of Semantics for the Validation of Numerical Programs. 59-77

Invited Talk

C. A. R. Hoare:
The Verifying Compiler, a Grand Challenge for Computing Research. 78-78

Verification I

Markus Müller-Olm, Oliver Rüthing, Helmut Seidl:
Checking Herbrand Equalities and Beyond. 79-96
Julien Bertrane:
Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs. 97-112
Aaron R. Bradley, Zohar Manna, Henny B. Sipma:
Termination of Polynomial Programs. 113-129
Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin:
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement. 130-145

Invited Talk

Amir Pnueli:
Abstraction for Liveness. 146-146

Heap and Shape Analysis

Bor-Yuh Evan Chang, K. Rustan M. Leino:
Abstract Interpretation with Alien Expressions and Heap Structures. 147-163
Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Shape Analysis by Predicate Abstraction. 164-180
Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv:
Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. 181-198
Alexandru Salcianu, Martin C. Rinard:
Purity and Side Effect Analysis for Java Programs. 199-215

Abstract Model Checking

Dennis Dams, Kedar S. Namjoshi:
Automata as Abstractions. 216-232
Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham:
Don't Know in the µ-Calculus. 233-249
A. Prasad Sistla, Min Zhou, Xiaodong Wang:
Model Checking of Systems Employing Commutative Functions. 250-266

Model Checking

Martin Lange:
Weak Automata for the Linear Time µ-Calculus. 267-281
Laura Bozzelli:
Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties. 282-297
ShengYu Shen, Ying Qin, Sikun Li:
Minimizing Counterexample with Unit Core Extraction and Incremental SAT. 298-312
Shahid Jabbar, Stefan Edelkamp:
I/O Efficient Directed Model Checking. 313-329

Applied Abstract Interpretation

Charles Hymans:
Verification of an Error Correcting Code by Abstract Interpretation. 330-345
Samir Genaim, Fausto Spoto:
Information Flow Analysis for Java Bytecode. 346-362
Jean Goubault-Larrecq, Fabrice Parrennes:
Cryptographic Protocol Analysis on Real C Code. 363-379

Bounded Model Checking

Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila:
Simple Is Better: Efficient Bounded Model Checking for Past LTL. 380-395
Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen:
Optimizing Bounded Model Checking for Linear Hybrid Systems. 396-412

Verification II

Stephen F. Siegel:
Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. 413-429
Patrick Lam, Viktor Kuncak, Martin C. Rinard:
Generalized Typestate Checking for Data Structure Consistency. 430-447
Nirman Kumar, Viraj Kumar, Mahesh Viswanathan:
On the Complexity of Error Explanation. 448-464
Paul C. Attie, Hana Chockler:
Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs. 465-481