Skip to main content
Conference ProceedingsOPEN ACCESS

Model checking in CLP

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (1999) 1579 223-239
DOI: 10.1007/3-540-49059-0_16
112Citations
Citations of this article
22Readers
Mendeley users who have this article in their library.

This article is free to access.

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 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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free