Model checking infinite-state systems in CLP

Delzanno, Giorgio; Podelski, Andreas

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Report

Model checking infinite-state systems in CLP

MPS-Authors

/persons/resource/persons44290

Delzanno, Giorgio
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45201

Podelski, Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

MPI-I-98-2-012.pdf
(Any fulltext), 493KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Delzanno, G., & Podelski, A.(1998). Model checking infinite-state systems in CLP (MPI-I-1998-2-012). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-7694-C

Abstract

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.