MPI-I-98-2-012
Model checking infinite-state systems in CLP
Delzanno, Giorgio and Podelski, Andreas
July 1998, 44 pages.
.
Status: available - back from printing
The verification of safety and liveness properties
for infinite-state systems is an important research problem. Can
the well-established concepts and the existing technology for
programming over constraints as first-class data structures
contribute to this research? The work reported in this paper is a
starting point for the experimental evaluation of constraint logic
programming as a conceptual basis and practical implementation
platform for model checking. We have implemented an automated
verification method in CLP using real and boolean constraints.
We have used the method on a number of infinite-state systems
that model concurrent programs using integers or buffers.
The basis of the correctness of our
implementation is a formal connection between CLP programs and the
formalism used for specifying concurrent systems.
-
- Attachement: MPI-I-98-2-012.ps (495 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1998-2-012
BibTeX
@TECHREPORT{DelzannoPodelski98,
AUTHOR = {Delzanno, Giorgio and Podelski, Andreas},
TITLE = {Model checking infinite-state systems in CLP},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-98-2-012},
MONTH = {July},
YEAR = {1998},
ISSN = {0946-011X},
}