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 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.
CITATION STYLE
Delzanno, G., & Podelski, A. (1999). Model checking in CLP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1579, pp. 223–239). Springer Verlag. https://doi.org/10.1007/3-540-49059-0_16
Mendeley helps you to discover research relevant for your work.