Verification, Model Checking, and Abstract Interpretation: Third International Workshop, VMCAI 2002 Venice, Italy, January 21–22, 2002 Revised Papers

Cinzia Bernardeschi, Nicoletta De Francesco (auth.), Agostino Cortesi (eds.)3540436316, 9783540436317

This book constitutes the thoroughly refereed post-proceedings of the Third International Workshop on Verification, Model Checking, and Abstract Interpretation, VMCAI 2002, held in Venice, Italy in January 2002.
The 22 revised full papers presented were carefully reviewed and selected from 41 submissions. The papers are organized in topical sections on security and protocols, timed systems and games, static analysis, optimization, types and verification, and temporal logics and systems.

---

Table of contents :
Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode….Pages 1-15
Proofs Methods for Bisimulation Based Information Flow Security….Pages 16-31
A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines….Pages 32-45
Analyzing Cryptographic Protocols in a Reactive Framework….Pages 46-64
An Abstract Schema for Equivalence-Checking Games….Pages 65-78
Synchronous Closing of Timed SDL Systems for Model Checking….Pages 79-93
Automata-Theoretic Decision of Timed Games….Pages 94-108
Compositional Termination Analysis of Symbolic Forward Analysis….Pages 109-125
Combining Norms to Prove Termination….Pages 126-138
Static Monotonicity Analysis for λ-definable Functions over Lattices….Pages 139-153
A Refinement of the Escape Property….Pages 154-166
Storage Size Reduction by In-place Mapping of Arrays….Pages 167-181
Verifying BDD Algorithms through Monadic Interpretation….Pages 182-195
Improving the Encoding of LTL Model Checking into SAT….Pages 196-207
Automatic Verification of Probabilistic Free Choice….Pages 208-224
An Experiment in Type Inference and Verification by Abstract Interpretation….Pages 225-239
Weak Muller Acceptance Conditions for Tree Automata….Pages 240-254
A Fully Abstract Model for Higher-Order Mobile Ambients….Pages 255-271
A Simulation Preorder for Abstraction of Reactive Systems….Pages 272-288
Approximating ATL * in ATL….Pages 289-301
Model Checking Modal Transition Systems Using Kripke Structures….Pages 302-316
Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness….Pages 317-330