Proceedings of the International Workshop on
Verification, Model Checking and Abstract Interpretation
held in conjunction with the
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".