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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Cortesi, Agostino (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
• Έκδοση: 1st ed. 2002.
• Σειρά: Lecture Notes in Computer Science, 2294
• Θέματα: Computers.; Software engineering.; Computer science.; Computer logic.; Programming languages (Electronic computers).; Theory of Computation.; Software Engineering/Programming and Operating Systems.; Computer Science, general.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.; Software Engineering.

Πίνακας περιεχομένων:

• 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.