Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, ProceedingsRadhia Cousot 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. |
Contents
| 1 | |
Numerical Abstraction | 25 |
The ArithmeticGeometric Progression Abstract Domain | 42 |
An Overview of Semantics for the Validation of Numerical Programs | 59 |
Invited Talk | 78 |
Static Analysis by Abstract Interpretation | 97 |
Termination of Polynomial Programs | 113 |
Verifying Safety of a Token Coherence Implementation | 130 |
Model Checking of Systems Employing Commutative Functions | 250 |
Weak Automata for the Linear Time μCalculus | 267 |
Model Checking for Process Rewrite Systems | 282 |
Minimizing Counterexample with Unit Core Extraction | 298 |
IO Efficient Directed Model Checking | 313 |
Applied Abstract Interpretation | 330 |
Information Flow Analysis for Java Bytecode | 346 |
Cryptographic Protocol Analysis on Real C Code | 363 |
Invited Talk | 146 |
Heap and Shape Analysis | 147 |
Shape Analysis by Predicate Abstraction | 164 |
Predicate Abstraction and Canonical Abstraction for SinglyLinked Lists | 181 |
Purity and Side Effect Analysis for Java Programs | 199 |
Automata as Abstractions | 216 |
Dont Know in the μCalculus | 233 |
Bounded Model Checking | 380 |
Optimizing Bounded Model Checking for Linear Hybrid Systems | 396 |
Verification II | 413 |
Generalized Typestate Checking for Data Structure Consistency | 430 |
On the Complexity of Error Explanation | 448 |
Efficiently Verifiable Conditions for DeadlockFreedom | 465 |
Other editions - View all
Verification, Model Checking, and Abstract Interpretation: 6th International ... Radhia Cousot No preview available - 2005 |
Verification, Model Checking, and Abstract Interpretation: 6th International ... Radhia Cousot No preview available - 2005 |
Common terms and phrases
abstract domain abstract interpretation algorithm analyze assertion assignment assume automata automatic differentiation automaton base domain bi-simulation boolean canonical abstraction clauses Computer Aided Verification concrete condition congruence-closure conjunction consider constraints counterexample Cousot cryptographic protocols data structures deadlock defined Definition denote e-graph edge encoding equivalent error example execution expression finite fixpoint formula given global graph heap Herbrand implementation infinite initial input integer invariant iteration Java bytecode Kripke structure language Lemma linear LNCS logic loop loop invariant Mealy machine method model checking node NuSMV operators optimization output parameter path Player PLTL polynomial predicate abstraction problem Proc Proof properties Proposition protocol prove rank function reachable refinement result Section semantics semidefinite programming simulation Springer-Verlag static analysis symbolic values termination Theorem tion transition relation transition systems typestate update variables verification VHDL VMCAI