Verification, Model Checking, and Abstract Interpretation

4th International Conference, VMCAI 2003 NewYork, NY, USA, January 9–11, 2003 Proceedings

  • Lenore D. Zuck
  • Paul C. Attie
  • Agostino Cortesi
  • Supratik Mukhopadhyay
Conference proceedings VMCAI 2003

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

Table of contents

  1. Front Matter
    Pages I-XI
  2. Invited Talks

  3. Invited Tutorials

    1. Bernhard Steffen, Hardi Hungar
      Pages 5-19
    2. Aravinda Prasad Sistla
      Pages 25-25
  4. Static Analysis

    1. Néstor Cataño, Marieke Huisman
      Pages 26-40
    2. Leena Unnikrishnan, Scott D. Stoller, Yanhong A. Liu
      Pages 70-85
  5. Dynamic Systems

    1. Chiara Braghin, Agostino Cortesi, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza
      Pages 86-101
  6. Abstract Interpretation

    1. Roberta Gori, Giorgio Levi
      Pages 132-145
    2. Roberto Giacobazzi, Isabella Mastroeni
      Pages 146-160
  7. Model Checking I

    1. Kedar S. Namjoshi
      Pages 174-188
    2. Patrice Godefroid, Radha Jagadeesan
      Pages 206-222
  8. Security Protocols

    1. Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi
      Pages 223-237
    2. Kazuhiro Ogata, Kokichi Futatsugi
      Pages 238-252
  9. Formal Methods

    1. Mila Majster-Cederbaum, Naijun Zhan, Harald Fecher
      Pages 253-267
    2. B. Meenakshi, R. Ramanujam
      Pages 268-282
    3. Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kýrlý, Nancy A. Lynch
      Pages 283-297
  10. Model Checking II

    1. Daniel Kroening, Ofer Strichman
      Pages 298-309
    2. Dennis Dams, Kedar S. Namjoshi
      Pages 310-323
  11. Back Matter
    Pages 325-325

About these proceedings


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.


Abstract Interpretation Concurrent Systems Model Checking Program Optimization Program Semantics Program Specification Program Verification Reactive Systems Simulation Temporal Logics algorithms complexity model construction structured analysis verification

Editors and affiliations

  • Lenore D. Zuck
    • 1
  • Paul C. Attie
    • 2
  • Agostino Cortesi
    • 3
  • Supratik Mukhopadhyay
    • 4
  1. 1.Department of Computer ScienceNew York UniversityNewYorkUSA
  2. 2.College of Computer ScienceNortheastern UniversityBostonUSA
  3. 3.Computer Science DepartmentVenice University C’FoscariMestre-VeneziaItaly
  4. 4.Department of Computer Science and Electrical EngineeringWest Virginia UniversityMorgantownUSA

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2003
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-540-00348-9
  • Online ISBN 978-3-540-36384-2
  • Series Print ISSN 0302-9743
  • Buy this book on publisher's site
Industry Sectors
Chemical Manufacturing
IT & Software
Consumer Packaged Goods
Finance, Business & Banking
Energy, Utilities & Environment