LEADER 03327oam 2200541 450 001 9910768192403321 005 20210512192050.0 010 $a3-540-47813-2 024 7 $a10.1007/3-540-47813-2 035 $a(CKB)1000000000211274 035 $a(SSID)ssj0000320626 035 $a(PQKBManifestationID)11254863 035 $a(PQKBTitleCode)TC0000320626 035 $a(PQKBWorkID)10249642 035 $a(PQKB)10995631 035 $a(DE-He213)978-3-540-47813-3 035 $a(MiAaPQ)EBC3062468 035 $a(MiAaPQ)EBC6408079 035 $a(PPN)123720311 035 $a(EXLCZ)991000000000211274 100 $a20210512d2002 uy 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 00$aVerification, model checking, and abstract interpretation $ethird international workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002 : revised papers /$fAgostino Cortesi (editor) 205 $a1st ed. 2002. 210 1$aBerlin, Germany ;$aNew York, New York :$cSpringer,$d[2002] 210 4$d©2002 215 $a1 online resource (VIII, 331 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2294 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-43631-6 320 $aIncludes bibliographical references and index. 327 $aSecurity 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. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v2294 606 $aComputer programs$xVerification$vCongresses 615 0$aComputer programs$xVerification 676 $a005.1/4 702 $aCortesi$b Agostino$f1963- 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bUtOrBLW 906 $aBOOK 912 $a9910768192403321 996 $aVerification, Model Checking, and Abstract Interpretation$92593983 997 $aUNINA