Verification, Model Checking and Abstract Interpretation

October 16 and 17, 1997, Port Jefferson, NY, USA

(A workshop in association with ILPS'97.)

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. 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. 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.
Clearly, among these three methods, there are similarities concerning their goals and their domains of applications.
Furthermore, while much research has been performed in the area of abstract interpretation of logic programs, connections between model checking and logic programming have hardly been investigated as yet; at the same time it seems that there may be interesting directions in this area. Besides model checking of (concurrent) logic programs, one may also think of the use of specialized constraint (logic) solvers to tackle the model checking problem.
The main goal of the workshop is to enhance cross-fertilization among these areas and in this way to clarify their relationships.

Organizing Committee

Annalisa Bossi (Coordinator)
University Ca' Foscari di Venezia, Italy.
Dennis Dams
Eindhoven Univ. of Technology, The Netherlands.
Gilberto File'
University of Padova, Italy.
Elena Marchiori
University Ca' Foscari di Venezia, Italy.

Workshop proceedings