Verkauf durch Sack Fachmedien

Cortesi

Verification, Model Checking, and Abstract Interpretation

Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers

Medium: Buch
ISBN: 978-3-540-43631-7
Verlag: Springer
Erscheinungstermin: 24.04.2002
Lieferfrist: bis zu 10 Tage

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.


Produkteigenschaften


  • Artikelnummer: 9783540436317
  • Medium: Buch
  • ISBN: 978-3-540-43631-7
  • Verlag: Springer
  • Erscheinungstermin: 24.04.2002
  • Sprache(n): Englisch
  • Auflage: Erscheinungsjahr 2002
  • Serie: Lecture Notes in Computer Science
  • Produktform: Kartoniert, Paperback
  • Gewicht: 1080 g
  • Seiten: 331
  • Format (B x H x T): 155 x 235 x 19 mm
  • Ausgabetyp: Kein, Unbekannt
Autoren/Hrsg.

Herausgeber

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.