Third International Workshop on
Verification, Model Checking and Abstract Interpretation


Call for papers

Program committe


Conference program


General Information









Call For Papers

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 workshop 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.

Topics include but are not limited to:

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

Important Dates:

Papers Submission Deadline: November 18, 2001
Notification of acceptance: December 16, 2001
Workshop : January 21-22, 2002, Venice, Italy
Final Version (Proceedings) : February 20, 2002

Paper Sumbission:

Authors are invited to submit an extended abstract ( 7 to 12 pages) by e-mail in PostScript format to cortesi@dsi.unive.it, following the LNCS guidelines.

At least one author of each accepted abstract is expected to attend the workshop.


Pre-proceedings will be available at the conference as a technical report of the University Ca' Foscari of Venice, Italy. It is planned to publish the post-proceedings in the Springer Lecture Notes in Computer Science series.