Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Modeling for Mere Mortals Read chapter Read first chapter

1999 | OriginalPaper | Chapter

Model Checking in CLP

Authors : Giorgio Delzanno, Andreas Podelski

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Included in: Professional Book Archive

Get Access

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

previous chapter Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol
next chapter Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets
Metadata
Title
Model Checking in CLP
Authors
Giorgio Delzanno
Andreas Podelski
Copyright Year
1999
Publisher
Springer Berlin Heidelberg
Book
Tools and Algorithms for the Construction and Analysis of Systems

Print ISBN: 978-3-540-65703-3

Electronic ISBN: 978-3-540-49059-3

Copyright Year: 1999

DOI
https://doi.org/10.1007/3-540-49059-0_16