000 03588nam a22005655i 4500
001 978-3-540-47813-3
003 DE-He213
005 20240423132544.0
007 cr nn 008mamaa
008 121227s2002 gw | s |||| 0|eng d
020 _a9783540478133
_9978-3-540-47813-3
024 7 _a10.1007/3-540-47813-2
_2doi
050 4 _aQA75.5-76.95
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a004.0151
_223
245 1 0 _aVerification, Model Checking, and Abstract Interpretation
_h[electronic resource] :
_bThird International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers /
_cedited by Agostino Cortesi.
250 _a1st ed. 2002.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2002.
300 _aVIII, 331 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v2294
505 0 _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.
650 0 _aComputer science.
650 0 _aSoftware engineering.
650 0 _aCompilers (Computer programs).
650 1 4 _aTheory of Computation.
650 2 4 _aSoftware Engineering.
650 2 4 _aComputer Science.
650 2 4 _aComputer Science Logic and Foundations of Programming.
650 2 4 _aCompilers and Interpreters.
700 1 _aCortesi, Agostino.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540436317
776 0 8 _iPrinted edition:
_z9783540829720
830 0 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v2294
856 4 0 _uhttps://doi.org/10.1007/3-540-47813-2
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
912 _aZDB-2-BAE
942 _cSPRINGER
999 _c189074
_d189074