Skip to main content
SpringerLink
Log in

Verification, Model Checking, and Abstract Interpretation

4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2003, Proceedings

  • Conference proceedings
  • © 2003

Overview

Editors:
  1. Lenore D. Zuck

    1. Department of Computer Science, New York University, NewYork, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Paul C. Attie

    1. College of Computer Science, Northeastern University, Boston, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Agostino Cortesi

    1. Computer Science Department, Venice University C’Foscari, Mestre-Venezia, Italy

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  4. Supratik Mukhopadhyay

    1. Department of Computer Science and Electrical Engineering, West Virginia University, Morgantown, USA

    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 2575)

Included in the following conference series:

Conference proceedings info: VMCAI 2003.

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 (25 papers)

  1. Front Matter

    Pages I-XI
    Download chapter PDF

  2. Invited Talks

    1. Software Model Checking with Abstraction Refinement

      • Andreas Podelski
      Pages 1-3

    2. Model-Checking and Abstraction to the Aid of Parameterized Systems

      • Amir Pnueli, Lenore Zuck
      Pages 4-4

  3. Invited Tutorials

    1. Behavior-Based Model Construction

      • Bernhard Steffen, Hardi Hungar
      Pages 5-19

    2. Automatic Verification by Abstract Interpretation

      • Patrick Cousot
      Pages 20-24

    3. Symmetry Reductions in Model-Checking

      • Aravinda Prasad Sistla
      Pages 25-25

  4. Static Analysis

    1. CHASE:A Static Checker for JML’s Assignable Clause

      • Néstor Cataño, Marieke Huisman
      Pages 26-40

    2. Abstract Interpretation-Based Certification of Assembly Code

      • Xavier Rival
      Pages 41-55

    3. Property Checking Driven Abstract Interpretation-Based Static Analysis

      • Damien Massé
      Pages 56-69

    4. Optimized Live Heap Bound Analysis

      • Leena Unnikrishnan, Scott D. Stoller, Yanhong A. Liu
      Pages 70-85

  5. Dynamic Systems

    1. Complexity of Nesting Analysis in Mobile Ambients

      • Chiara Braghin, Agostino Cortesi, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza
      Pages 86-101

    2. Types for Evolving Communication in Safe Ambients

      • Francesca Levi
      Pages 102-115

    3. A Logical Encoding of the π-Calculus: Model Checking Mobile Processes Using Tabled Resolution

      • Ping Yang, C.R. Ramakrishnan, Scott A. Smolka
      Pages 116-131

  6. Abstract Interpretation

    1. Properties of a Type Abstract Interpreter

      • Roberta Gori, Giorgio Levi
      Pages 132-145

    2. Domain Compression for Complete Abstractions

      • Roberto Giacobazzi, Isabella Mastroeni
      Pages 146-160

    3. Abstraction of Expectation Functions Using Gaussian Distributions

      • David Monniaux
      Pages 161-173

  7. Model Checking I

    1. Lifting Temporal Proofs through Abstractions

      • Kedar S. Namjoshi
      Pages 174-188

    2. Efficient Verification of Timed Automata with BDD-Like Data-Structures

      • Farn Wang
      Pages 189-205

    3. On the Expressiveness of 3-Valued Models

      • Patrice Godefroid, Radha Jagadeesan
      Pages 206-222

  8. Security Protocols

    1. Bisimulation and Unwinding for Verifying Possibilistic Security Properties

      • Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi
      Pages 223-237
Back to top

Other volumes

  1. Verification, Model Checking, and Abstract Interpretation

Keywords

About this book

This volume contains the proceedings of the 4th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2003), held in New York city, January 9–11, 2003. The purpose of VMCAI was to provide a forum for researchers from three communities—Veri?cation, Model Checking, and Abstract Interpretation—that will facilitate interaction, cross-fertilization, and the advance of hybrid methods that combine the three areas. With the g- wingneedforformaltoolstoreasonaboutcomplex,in?nite-state,andembedded systems, such hybrid methods are bound to be of great importance. Topics covered by VMCAI include program veri?cation, static analysis te- niques, model checking, program certi?cation, type systems, abstract domains, debugging techniques, compiler optimization, embedded systems, and formal analysis of security protocols. VMCAI 2003 was the fourth VMCAI meeting. The previous three were held as workshops (Port Je?erson 1997, Pisa 1998, and Venice 2002). It is the success of the last meeting, and the wide response it generated, that made it clear the time had come to make it an annual conference.

Editors and Affiliations

  • Department of Computer Science, New York University, NewYork, USA

    Lenore D. Zuck

  • College of Computer Science, Northeastern University, Boston, USA

    Paul C. Attie

  • Computer Science Department, Venice University C’Foscari, Mestre-Venezia, Italy

    Agostino Cortesi

  • Department of Computer Science and Electrical Engineering, West Virginia University, Morgantown, USA

    Supratik Mukhopadhyay

Bibliographic Information

  • Book Title: Verification, Model Checking, and Abstract Interpretation

  • Book Subtitle: 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2003, Proceedings

  • Editors: Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, Supratik Mukhopadhyay

  • Series Title: Lecture Notes in Computer Science

  • DOI: https://doi.org/10.1007/3-540-36384-X

  • Publisher: Springer Berlin, Heidelberg

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer-Verlag Berlin Heidelberg 2003

  • Softcover ISBN: 978-3-540-00348-9Published: 13 December 2002

  • eBook ISBN: 978-3-540-36384-2Published: 01 July 2003

  • Series ISSN: 0302-9743

  • Series E-ISSN: 1611-3349

  • Edition Number: 1

  • Number of Pages: XII, 328

  • Topics: Software Engineering, Logics and Meanings of Programs, Programming Languages, Compilers, Interpreters

Publish with us

Policies and ethics

Back to top

Search

Navigation