Verification, Model Checking, and Abstract Interpretation

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.

Inhalt

Security and Protocols.- Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode.- Proofs Methods for Bisimulation Based Information Flow Security.- A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines.- Analyzing Cryptographic Protocols in a Reactive Framework.- Timed Systems and Games.- An Abstract Schema for Equivalence-Checking Games.- Synchronous Closing of Timed SDL Systems for Model Checking.- Automata-Theoretic Decision of Timed Games.- Static Analysis.- Compositional Termination Analysis of Symbolic Forward Analysis.- Combining Norms to Prove Termination.- Static Monotonicity Analysis for ?-definable Functions over Lattices.- A Refinement of the Escape Property.- Optimizations.- Storage Size Reduction by In-place Mapping of Arrays.- Verifying BDD Algorithms through Monadic Interpretation.- Improving the Encoding of LTL Model Checking into SAT.- Types and Verification.- Automatic Verification of Probabilistic Free Choice.- An Experiment in Type Inference and Verification by Abstract Interpretation.- Weak Muller Acceptance Conditions for Tree Automata.- A Fully Abstract Model for Higher-Order Mobile Ambients.- Temporal Logics and Systems.- A Simulation Preorder for Abstraction of Reactive Systems.- Approximating ATL* in ATL.- Model Checking Modal Transition Systems Using Kripke Structures.- Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness.