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

2002-12  

湖南文艺出版社  

Cortesi, Agostino  

330  

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.

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

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