Verification, Model Checking, and Abstract Interpretation

Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers

348 Seiten, Taschenbuch

Kurzbeschreibung des Verlags

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.

• Reihe: Lecture Notes in Computer Science
• Themen: Informatik und Informationstechnologie Informatik Theoretische Informatik
• ISBN: 9783540436317
• Sprache: Englisch
• Erscheinungsdatum: 24.04.2002
• Größe: 235 x 155 mm
• Verlag: Springer
• Herausgegeben von: Agostino Cortesi