验证、模型检验与抽象解读/Verification, model checking, and abstract interpretatio

书籍目录

Security and Protocols  Combining Abstract Interpretation and Model Checking for Security Properties of Java BytecodeAnalysing  Proofs Methods for Bisimulation Based Information Flow Security  A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines Sou8a  Analyzing Cryptographic Protocols in a Reactive FrameworkTimed Systems and Games  An Abstract Schema for Equivalence-Checking Games  Synchronous Closing of Timed SDL Systems for Model Checking  Automata-Theoretic Decision of Timed GamesStatic Analysis  Compositional Termination Analysis of Symbolic Forward Analysis  Combining Norms to Prove Termination  Static Monotonicity Analysis for h-definable Functions over Lattices  A Refinement of the Escape PropertyOptimizations  Storage Size Reduction by  In-place Mapping of Arrays  Verifying BDD Algorithms through Monadic InterpretationImproving 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 AmbientsTemporal 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 LivenessAuthor Index

作者简介

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.

 验证、模型检验与抽象解读/Verification, model checking, and abstract interpretatio下载