03325oam 2200541 450 99646556420331620210512192050.03-540-47813-210.1007/3-540-47813-2(CKB)1000000000211274(SSID)ssj0000320626(PQKBManifestationID)11254863(PQKBTitleCode)TC0000320626(PQKBWorkID)10249642(PQKB)10995631(DE-He213)978-3-540-47813-3(MiAaPQ)EBC3062468(MiAaPQ)EBC6408079(PPN)123720311(EXLCZ)99100000000021127420210512d2002 uy 0engurnn#008mamaatxtccrVerification, model checking, and abstract interpretation third international workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002 : revised papers /Agostino Cortesi (editor)1st ed. 2002.Berlin, Germany ;New York, New York :Springer,[2002]©20021 online resource (VIII, 331 p.)Lecture Notes in Computer Science,0302-9743 ;2294Bibliographic Level Mode of Issuance: Monograph3-540-43631-6 Includes bibliographical references and index.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.Lecture Notes in Computer Science,0302-9743 ;2294Computer programsVerificationCongressesComputer programsVerification005.1/4Cortesi Agostino1963-MiAaPQMiAaPQUtOrBLWBOOK996465564203316Verification, Model Checking, and Abstract Interpretation2593983UNISA