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)
bossi@dsi.unive.it
University Ca' Foscari di Venezia, Italy.
Dennis Dams
wsindd@win.tue.nl
Eindhoven Univ. of Technology, The Netherlands.
Gilberto File'
gilberto@math.unipd.it
University of Padova, Italy.
Elena Marchiori
elena@dsi.unive.it
University Ca' Foscari di Venezia, Italy.