Vai al contenuto principale della pagina
| Titolo: |
Verification, model checking, and abstract interpretation : third international workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002 : revised papers / / Agostino Cortesi (editor)
|
| Pubblicazione: | Berlin, Germany ; ; New York, New York : , : Springer, , [2002] |
| ©2002 | |
| Edizione: | 1st ed. 2002. |
| Descrizione fisica: | 1 online resource (VIII, 331 p.) |
| Disciplina: | 005.1/4 |
| Soggetto topico: | Computer programs - Verification |
| Persona (resp. second.): | CortesiAgostino <1963-> |
| Note generali: | Bibliographic Level Mode of Issuance: Monograph |
| Nota di bibliografia: | Includes bibliographical references and index. |
| Nota di contenuto: | 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. |
| Titolo autorizzato: | Verification, Model Checking, and Abstract Interpretation ![]() |
| ISBN: | 3-540-47813-2 |
| Formato: | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione: | Inglese |
| Record Nr.: | 996465564203316 |
| Lo trovi qui: | Univ. di Salerno |
| Opac: | Controlla la disponibilità qui |