Proceedings of the International Workshop on



Verification, Model Checking and Abstract Interpretation



Annalisa Bossi (editor)





held in conjunction with the

International Logic Programming Symposium 1997





October 16 and 17, 1997, Port Jefferson, Long Island N.Y., USA.




Also available as Report CS97-14, Ottobre 1997
Dipartimento di Matematica Applicata ed Informatica
Universita' Ca' Foscari di Venezia, Italy



Preface

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.


Workshop schedule

Thursday, October 16, 1997
14.00 - 15.30
  • A Reconstruction of Verification Techniques by Abstract Interpretation
    P. Volpe and G. Levi
  • Relating Abstract Interpretation with Logic Program verification
    M.M. Gallardo, P. Merino and J.M. Troya
  • It is Declarative
    W. Drabent
15.30 - 16.00
Open Discussion and Coffee Break
16.00 - 17.30
  • Fine-Grained Goal-Dependent Declarative Analysis of Logic programs
    D. Boulanger
  • Interprocedural Analysis Based on PDAs
    H.Seidl and C. Fecht
  • A Verification Calculus for the TAO Coordination Model
    L. Semini and L. Monteiro
17.30 - 18.00
Open Discussion
Friday, October 17, 1997
9.00 - 10.30
  • Efficient Model Checking Using Tabled Resolution
    Y.S. Ramakrishna, C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, T. Swift and D.S. Warren (invited talk)
  • Limiting State Explosion with Filter-Based Refinement
    M.B. Dwyer and D.A. Schmidt
  • Abstract Model Checking of Value-passing Processes
    F. Levi
10.30 - 11.15
Open Discussion and Coffee Break
11.15 - 12.15
  • Compositional Verification of Knowledge-Based Systems in Temporal Epistemic Logic
    J. Treur, J. Engelfriet and C. Jonker
  • A Constrained-based Approach for Specification and Verification of Real-time Systems
    E. Pontelli and G. Gupta
12.15 - 13.00
Open Discussion and Closing



Contributions


A Reconstruction of Verification Techniques by Abstract Interpretation
P. Volpe and G. Levi

Relating Abstract Interpretation with Logic Program verification
M.M. Gallardo, P. Merino and J.M. Troya

It is Declarative
W. Drabent

Fine-Grained Goal-Dependent Declarative Analysis of Logic programs
D. Boulanger

Interprocedural Analysis Based on PDAs
H.Seidl and C. Fecht

A Verification Calculus for the TAO Coordination Model
L. Semini and L. Monteiro

Limiting State Explosion with Filter-Based Refinement
M.B. Dwyer and D.A. Schmidt

Abstract Model Checking of Value-passing Processes
F. Levi

Compositional Verification of Knowledge-Based Systems in Temporal Epistemic Logic
J. Treur, J. Engelfriet and C. Jonker

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

The invited paper 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
appeared in the proceedings of "Computer Aided Verification 1997".