MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Delzanno, Giorgio
Podelski, Andreas		dblp
dblp
Editor(s):
Cleaveland, Rancedblp
BibTeX cite key*:
Podelski1998
Title, Booktitle
Title*:
Model Checking in CLP
Booktitle*:
Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS-99)
Event, URLs
Conference URL::
http://www.cwi.nl/conferences/ETAPS99.html
Downloading URL:
Event Address*:
Amsterdam, The Netherlands
Language:
English
Event Date*
(no longer used):
March, 22nd-26th
Organization:
European Association for Programming Languages and Systems (EAPLS); European Association for Theoretical Computer Science (EATCS)
Event Start Date:
14 May 2024
Event End Date:
14 May 2024
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
1579
Number:
Month:
January
Pages:
223-239
Year*:
1999
VG Wort Pages:
ISBN/ISSN:
3-540-65703-7
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) 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.
Keywords:
Model Checking, Constraint Logic Programs
Download
Access Level:

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat



BibTeX Entry:
@INPROCEEDINGS{Podelski1998,
AUTHOR = {Delzanno, Giorgio and Podelski, Andreas},
 EDITOR = {Cleaveland, Rance},
 TITLE = {Model Checking in {CLP}},
 BOOKTITLE = {Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS-99)},
 PUBLISHER = {Springer},
 YEAR = {1999},
 ORGANIZATION = {European Association for Programming Languages and Systems (EAPLS); European Association for Theoretical Computer Science (EATCS)},
 VOLUME = {1579},
 PAGES = {223--239},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Amsterdam, The Netherlands},
 MONTH = {January},
 ISBN = {3-540-65703-7},
}

Entry last modified by Uwe Brahm, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Andreas Podelski		Created
01/18/1999 05:09:14 PM
Revisions
13.
12.
11.
10.
9.		Editor(s)
Uwe Brahm
Giorgio Delzanno
Giorgio Delzanno
Giorgio Delzanno
Giorgio Delzanno		Edit Dates
28.03.2000 10:43:11
22/04/99 12:18:57
22/04/99 12:16:01
22/04/99 10:42:45
22/04/99 10:41:03