Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Model checking infinite-state systems 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)

MPI-I-98-2-012.pdf
(beliebiger Volltext), 493KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-7694-C
Zusammenfassung
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.