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): Radhia Cousot
Edition: 1
Year: 2005
Language: English
Pages: 495
354024297X......Page 1
Table of Contents......Page 10
Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming......Page 14
Scalable Analysis of Linear Systems Using Mathematical Programming......Page 38
The Arithmetic-Geometric Progression Abstract Domain......Page 55
An Overview of Semantics for the Validation of Numerical Programs......Page 72
The Verifying Compiler, a Grand Challenge for Computing Research......Page 91
Checking Herbrand Equalities and Beyond......Page 92
Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs......Page 110
Termination of Polynomial Programs......Page 126
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement......Page 143
Abstraction for Liveness......Page 159
Abstract Interpretation with Alien Expressions and Heap Structures......Page 160
Shape Analysis by Predicate Abstraction......Page 177
Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists......Page 194
Purity and Side Effect Analysis for Java Programs......Page 212
Automata as Abstractions......Page 229
Don’t Know in the μ-Calculus......Page 246
Model Checking of Systems Employing Commutative Functions......Page 263
Weak Automata for the Linear Time μ-Calculus......Page 280
Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties......Page 295
Minimizing Counterexample with Unit Core Extraction and Incremental SAT......Page 311
I/O Efficient Directed Model Checking......Page 326
Verification of an Error Correcting Code by Abstract Interpretation......Page 343
Information Flow Analysis for Java Bytecode......Page 359
Cryptographic Protocol Analysis on Real C Code......Page 376
Simple Is Better: Efficient Bounded Model Checking for Past LTL......Page 393
Optimizing Bounded Model Checking for Linear Hybrid Systems......Page 409
Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives......Page 426
Generalized Typestate Checking for Data Structure Consistency......Page 443
On the Complexity of Error Explanation......Page 461
Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs......Page 478
Author Index......Page 496
