The book constitutes the refereed proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2005, held in Paris, France in January 2005.
The 27 revised full papers presented together with an invited paper were carefully reviewed and selected from 92 submissions. The papers are organized in topical sections on numerical abstraction, verification, heap and shape analysis, abstract model checking, model checking, applied abstract interpretation, and bounded model checking.
Author(s): Patrick Cousot (auth.), Radhia Cousot (eds.)
Series: Lecture Notes in Computer Science 3385 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005
Language: English
Pages: 483
Tags: Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Software Engineering
Front Matter....Pages -
Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming....Pages 1-24
Scalable Analysis of Linear Systems Using Mathematical Programming....Pages 25-41
The Arithmetic-Geometric Progression Abstract Domain....Pages 42-58
An Overview of Semantics for the Validation of Numerical Programs....Pages 59-77
The Verifying Compiler, a Grand Challenge for Computing Research....Pages 78-78
Checking Herbrand Equalities and Beyond....Pages 79-96
Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs....Pages 97-112
Termination of Polynomial Programs....Pages 113-129
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement....Pages 130-145
Abstraction for Liveness....Pages 146-146
Abstract Interpretation with Alien Expressions and Heap Structures....Pages 147-163
Shape Analysis by Predicate Abstraction....Pages 164-180
Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists....Pages 181-198
Purity and Side Effect Analysis for Java Programs....Pages 199-215
Automata as Abstractions....Pages 216-232
Don’t Know in the μ -Calculus....Pages 233-249
Model Checking of Systems Employing Commutative Functions....Pages 250-266
Weak Automata for the Linear Time μ -Calculus....Pages 267-281
Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties....Pages 282-297
Minimizing Counterexample with Unit Core Extraction and Incremental SAT....Pages 298-312
I/O Efficient Directed Model Checking....Pages 313-329
Verification of an Error Correcting Code by Abstract Interpretation....Pages 330-345
Information Flow Analysis for Java Bytecode....Pages 346-362
Cryptographic Protocol Analysis on Real C Code....Pages 363-379
Simple Is Better: Efficient Bounded Model Checking for Past LTL....Pages 380-395
Optimizing Bounded Model Checking for Linear Hybrid Systems....Pages 396-412
Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives....Pages 413-429
Generalized Typestate Checking for Data Structure Consistency....Pages 430-447
On the Complexity of Error Explanation....Pages 448-464
Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs....Pages 465-481
Back Matter....Pages -
