LEADER 03325oam  2200541   450 
001 996465564203316
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   $a996465564203316
996   $aVerification, Model Checking, and Abstract Interpretation$92593983
997   $aUNISA