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

Bibliographic Details
Other Authors: Cortesi, Agostino (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 2002, 2002
Edition:1st ed. 2002
Series:Lecture Notes in Computer Science
Subjects:
Online Access:
Collection: Springer Book Archives -2004 - Collection details see MPG.ReNa
LEADER 02777nmm a2200337 u 4500
001 EB000658117
003 EBX01000000000000001349408
005 00000000000000.0
007 cr|||||||||||||||||||||
008 140122 ||| eng
020 |a 9783540478133 
100 1 |a Cortesi, Agostino  |e [editor] 
245 0 0 |a Verification, Model Checking, and Abstract Interpretation  |h Elektronische Ressource  |b Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers  |c edited by Agostino Cortesi 
250 |a 1st ed. 2002 
260 |a Berlin, Heidelberg  |b Springer Berlin Heidelberg  |c 2002, 2002 
300 |a VIII, 331 p  |b online resource 
505 0 |a 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 
653 |a Compilers (Computer programs) 
653 |a Computer Science Logic and Foundations of Programming 
653 |a Compilers and Interpreters 
653 |a Software engineering 
653 |a Computer science 
653 |a Computer Science 
653 |a Software Engineering 
653 |a Theory of Computation 
041 0 7 |a eng  |2 ISO 639-2 
989 |b SBA  |a Springer Book Archives -2004 
490 0 |a Lecture Notes in Computer Science 
028 5 0 |a 10.1007/3-540-47813-2 
856 4 0 |u https://doi.org/10.1007/3-540-47813-2?nosfx=y  |x Verlag  |3 Volltext 
082 0 |a 40,151