Fifth International Conference on

Verification, Model Checking and Abstract Interpretation


Conference Announcement

Call for Papers

Program Committee

Conference program



General Information

A note by David Harel











January 11-13, 2004
Auditorium S.Margherita - Venice, Italy

in cooperation with ACM POPL
sponsored by EAPLS

Registration is through the POPL 2004 web pages
List of Accepted Papers

The Fifth International Conference on Verification, Model Checking and Abstract Interpretation follows the successful events held in Port Jefferson (1997), Pisa (1998), Venice (2002), and New York (2003).

Motivations and Goals

Program verification aims at proving that programs meet their specifications, i.e., that the actual program behaviour coincides with the desired one.
Model checking is a specific approach to the verification of temporal properties of reactive and concurrent systems, which has proven successful in the area of finite-state programs.
Abstract interpretation is a method for designing and comparing semantics of programs, expressing various types of programs properties; in particular, it has been successfully used to infer run-time program properties that can be valuable to optimize programs.
Clearly, among these three methods, there are similarities concerning their goals and their domains of applications. The main goal of the conference is that of enhancing cross-fertilization among these areas and in this way to clarify their relationships.

Papers are solicited, reporting on the use of techniques for deriving or proving properties of programs and more generally of finite dynamic systems. Contributions examining the relations among the different techniques will be considered particularly interesting. Description of work in progress is also welcome.

The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series (as in the last editions of the Conference).

Topics include but are not limited to:

  • program verification
  • static analysis techniques
  • model checking
  • program certification
  • type systems
  • abstract domains
  • debugging techniques
  • compiler optimization.
  • embedded systems
  • security


Invited Speakers

David Harel (Weizmann, IL)

Dawson Engler (Stanford University, USA)

Mooly Sagiv (Tel Aviv University, IL),


Joshua Guttman (Mitre, USA)

Program co-chairs

Giorgio Levi

University of Pisa

Bernhard Steffen

University of Dortmund


Steering Committee

Agostino Cortesi

Univ. Ca' Foscari (I)

E. Allen Emerson

University of Texas, Austin (USA)

Giorgio Levi

University of Pisa (I)

Andreas Podelski

Max Planck Institute (D)

Thomas W. Reps

University of Wisconsin, Madison (USA)

David A. Schmidt

Kansas State University (USA)

Lenore Zuck

New York University (USA)