Checking and Abstract Interpretation
A Post-Conference Workshop of ILPS'97
The first workshop on Verification,
Model Checking and Abstract Interpretation took place in Port Jefferson, N.Y., on October
16 and 17, 1997.
The organizing committee was formed by
Annalisa Bossi (University Ca' Foscari of Venice, Italy), Dennis Dams (Eindhoven
University of Technology, The Netherlands), Gilberto File (University of Padova, Italy)
and Elena Marchiori (University Ca' Foscari of Venice, Italy).
The objective of the workshop was to
bring together researchers from the areas of program verification, model checking and
abstract interpretation, in order to enhance cross-fertilization and to clarify the
relationships among the three areas.
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. Program verification aims at proving
that programs meet their specifications, i.e., that the actual program behaviour coincides
with the desired one. Both techniques have been widely used for the study of properties of
logic programs and can be seen as dual approaches to the same problem. Model checking is a
specific approach to the verification of reactive and concurrent systems, which has proven
successful in the area of finite-state programs. Being a general technique, it also
applies to finite-state programs expressed through the logic programming paradigm.
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.
Eleven papers have been accepted for
presentation at the workshop. The main topics covered by the
contributions are: comparison of abstract interpretation and verification of logic
programs as well as comparison of various approaches to the verification of logic
programs; abstract model checking; implementation of a model checker in a logic
programming system; techniques for verification, abstract interpretation and
model-checking applied to concurrent languages; formalisms for the verification of systems
where the notion of time is relevant; frameworks and tools for fine-grained analysis of
logic programs and interprocedural analysis of imperative and logic programs.
- Reconstruction of Verification
Techniques by Abstract Interpretation by P. Volpe and G. Levi.
- Relating Abstract Interpretation with
Logic Program verification by M.M. Gallardo, P. Merino and J.M. Troya
- It is Declarative by W. Drabent.
- Fine-Grained Goal-Dependent
Declarative Analysis of Logic programs by D. Boulanger.
- Interprocedural Analysis Based on
PDAs by H.Seidl and C. Fecht.
- A Verification Calculus for the TAO
Coordination Model by L. Semini and L. Monteiro.
- Efficient Model Checking Using Tabled
Resolution by Y.S. Ramakrishna, C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, T.
Swift and D.S. Warren.
- Limiting State Explosion with
Filter-Based Refinement by M.B. Dwyer and D.A. Schmidt.
- Abstract Model Checking of
Value-passing Processes by F. Levi.
- Compositional Verification of
Knowledge-Based Systems in Temporal Epistemic Logic by J. Treur, J. Engelfriet and C.
- A Constrained-based Approach for
Specification and Verification of Real-time Systems by E. Pontelli and G. Gupta.