Model Checking in CLP

Delzanno, Giorgio; Podelski, Andreas

Datensatz

DATENSATZ AKTIONENEXPORT

Zur Ablage hinzufügen

Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben

Konferenzbeitrag

Model Checking in CLP

MPG-Autoren

/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;

Externe Ressourcen

Es sind keine externen Ressourcen hinterlegt

Volltexte (beschränkter Zugriff)

Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.

Volltexte (frei zugänglich)

Es sind keine frei zugänglichen Volltexte in PuRe verfügbar

Ergänzendes Material (frei zugänglich)

Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

Zitation

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.

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

Zusammenfassung

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.