Model Checking in CLP

Delzanno, Giorgio; Podelski, Andreas

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Model Checking 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)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Delzanno, G., & Podelski, A. (1999). Model Checking in CLP. In R. Cleaveland (Ed.), Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS-99) (pp. 223-239). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-365F-0

Abstract

We show that Constraint Logic Programming (CLP) can serve as a conceptual basis and as a practical implementation platform for the model checking of infinite-state systems. Our contributions are: (1)~a semantics-preserving translation of \emph{concurrent systems} into CLP programs, (2)~a method for verifying safety and liveness properties on the CLP programs produced by the translation. We have implemented the method in a CLP system and verified well-known examples of infinite-state programs over integers, using here linear constraints as opposed to Presburger arithmetic as in previous solutions.