Skip to main content
SpringerLink
Log in
Book cover

Verification, Model Checking, and Abstract Interpretation

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

  • Conference proceedings
  • © 2002

Overview

Editors:
  1. Agostino Cortesi

    1. Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Mestre-Venezia, Italy

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 2294)

Included in the following conference series:

Conference proceedings info: VMCAI 2002.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (22 papers)

  1. Front Matter

    Pages I-VIII
    Download chapter PDF

  2. Security and Protocols

    1. Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode

      • Cinzia Bernardeschi, Nicoletta De Francesco
      Pages 1-15

    2. Proofs Methods for Bisimulation Based Information Flow Security

      • Riccardo Focardi, Carla Piazza, Sabina Rossi
      Pages 16-31

    3. A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines

      • Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa
      Pages 32-45

    4. Analyzing Cryptographic Protocols in a Reactive Framework

      • R. K. Shyamasundar
      Pages 46-64

  3. Timed Systems and Games

    1. An Abstract Schema for Equivalence-Checking Games

      • Li Tan
      Pages 65-78

    2. Synchronous Closing of Timed SDL Systems for Model Checking

      • Natalia Sidorova, Martin Steffen
      Pages 79-93

    3. Automata-Theoretic Decision of Timed Games

      • Marco Faella, Salvatore La Torre, Aniello Murano
      Pages 94-108

  4. Static Analysis

    1. Compositional Termination Analysis of Symbolic Forward Analysis

      • Witold Charatonik, Supratik Mukhopadhyay, Andreas Podelski
      Pages 109-125

    2. Combining Norms to Prove Termination

      • Samir Genaim, Michael Codish, John Gallagher, Vitaly Lagoon
      Pages 126-138

    3. Static Monotonicity Analysis for λ-definable Functions over Lattices

      • Andrzej S. Murawski, Kwangkeun Yi
      Pages 139-153

    4. A Refinement of the Escape Property

      • Patricia M. Hill, Fausto Spoto
      Pages 154-166

  5. Optimizations

    1. Storage Size Reduction by In-place Mapping of Arrays

      • Remko Tronçon, Maurice Bruynooghe, Gerda Janssens, Francky Catthoor
      Pages 167-181

    2. Verifying BDD Algorithms through Monadic Interpretation

      • Sava Krstić, John Matthews
      Pages 182-195

    3. Improving the Encoding of LTL Model Checking into SAT

      • Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani
      Pages 196-207

  6. Types and Verification

    1. Automatic Verification of Probabilistic Free Choice

      • Lenore Zuck, Amir Pnueli, Yonit Kesten
      Pages 208-224

    2. An Experiment in Type Inference and Verification by Abstract Interpretation

      • Roberta Gori, Giorgio Levi
      Pages 225-239

    3. Weak Muller Acceptance Conditions for Tree Automata

      • Salvatore La Torre, Aniello Murano, Margherita Napoli
      Pages 240-254

    4. A Fully Abstract Model for Higher-Order Mobile Ambients

      • Mario Coppo, Mariangiola Dezani-Ciancaglini
      Pages 255-271

  7. Temporal Logics and Systems

    1. A Simulation Preorder for Abstraction of Reactive Systems

      • Ferucio Laurentţiu TŢiplea, Aurora TŢiplea
      Pages 272-288
Back to top

Other volumes

  1. Verification, Model Checking, and Abstract Interpretation

Keywords

Editors and Affiliations

  • Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Mestre-Venezia, Italy

    Agostino Cortesi

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation