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

Cortesi, Agostino

ISBN 10: 3540436316 / ISBN 13: 9783540436317

Editore: Springer 2002-04, 2002

Riguardo questo articolo

Codice articolo 6666-IUK-9783540436317

Dati bibliografici

• Titolo: Verification, Model Checking, and Abstract Interpretation : Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Pape
• Editore: Springer 2002-04
• Data di pubblicazione: 2002
• Lingua: Inglese
• ISBN 10: 3540436316
• ISBN 13: 9783540436317
• Rilegatura: PF
• Condizione: New

Descrizione articolo

Riassunto

projectofmakingVMCAI anannualprivilegedforumfor researchersin the area. Specialthanksareduetotheinstitutionsthatsponsoredtheevent:theC- puter Science Department of the University Ca Foscari, the European Asso- ation for Programming Languages and Systems (EAPLS), the MIUR Project InterpretazioneAstratta,TypeSystemseAnalisiControl-Flow andtheMIUR Project MetodiFormaliperlaSicurezza-MEFISTO .Weareespeciallygra- ful to C. Braghin for her helpful support in organizingthe workshop.

Contenuti

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.