Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings (Lecture Notes in Computer Science)

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. 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 - Program verification is based on reasonings by induction (e.g. on program steps) which involves the discovery of unknown inductive arguments (e.g. rank functions, invariants) satisfying universally quantified verification conditions.