A Post-Conference Workshop of ILPS'97

Annalisa Bossi

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.

References

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

- A Constrained-based Approach for Specification and Verification of Real-time Systems by E. Pontelli and G. Gupta.