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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. A. Abdulla, K. Čerāns, B. Jonsson, and Y.-K. Tsay. General Decidability Theorems for Infinite-state Systems. In Proceedings of the Eleventh Annual Symposium on Logic in Computer Science (LICS’96), pages 313–321. IEEE Computer Society Press, 1996.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In John C. Mitchell, editor, Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS’90), pages 428–439. IEEE Society Press, 1990.
T. Bultan, R. Gerber, and C. League. Verifying Systems with Integer Constraints and Boolean Predicates: a Composite Approach. In Proceedings of the 1998 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’98), pages 113–123. ACM Press, 1998.
T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinitestate Systems using Presburger Arithmetics. In Orna Grumberg, editor, Proceedings of the Ninth Conference on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 400–411. Springer-Verlag, 1997.
T. Bultan, R. Gerber, and W. Pugh. Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results. Technical Report CS-TR-3870, UMIACSTR-98-07, Department of Computer Science, University of Maryland, College Park, 1998.
B. Boigelot and P. Wolper. Symbolic Verification with Periodic Sets. In David Dill, editor, Proceedings of the Sixth International Conference on Computer Aided Verification (CAV’94), volume 818 of LNCS, pages 55–67. Springer-Verlag, 1994.
B. Boigelot and P. Wolper. Verifying Systems with Infinite but Regular State Space. In Alan J. Hu and Moshe Y. Vardi, editors, Proceedings of the Tenth Conference on Computer Aided Verification (CAV’98), volume 1427 of LNCS, pages 88–97. Springer-Verlag, 1998.
W. Chan, R. Anderson, P. Beame, and D. Notkin. Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Nonlinear Constraints. In Orna Grumberg, editor, Proceedings of the Ninth Conference on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 316–327. Springer-Verlag, 1997.
P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints among Variables of a Program. In Proceedings of the Fifth Annual Symposium on Principles of Programming Languages (POPL’78), pages 84–96. ACM Press, 1978.
H. Comon and Y. Jurski. Multiple Counters Automata, Safety Analysis, and Presburger Arithmetics. In Alan J. Hu and M. Y. Vardi, editors, Proceedings of the Tenth Conference on Computer Aided Verification (CAV’98), volume 1427 of LNCS, pages 268–279. Springer-Verlag, 1998.
W. Charatonik and A. Podelski. Set-based Analysis of Reactive Infinite-state Systems. In Bernhard Steffen, editor, Proceedings of of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), volume 1384 of LNCS, pages 358–375. Springer-Verlag, 1998.
E. A. Emerson. Temporal and Modal Logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995–1072. Elsevier Science, 1990.
L. Fribourg and H. Olsen. A Decompositional Approach for Computing Least Fixed Point of Datalog Programs with Z-counters. Journal of Constraints, 2(3-4):305–336, 1997.
L. Fribourg and J. Richardson. Symbolic Verification with Gap-order Constraints. Technical Report LIENS-93-3, Laboratoire d’Informatique, Ecole Normale Superieure, Paris, 1996.
M. Gabbrielli, M. G. Dore, and G. Levi. Observable Semantics for Constraint Logic Programs. Journal of Logic and Computation, 2(5):133–171, 1995.
G. Gupta and E. Pontelli. A Constraint Based Approach for Specification and Verification of Real-time Systems. In Proceedings of the 18th IEEE Real Time Systems Symposium (RTSS’97). IEEE Computer Society, 1997.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a Model Checker for Hybrid Systems. In Orna Grumberg, editor, Proceedings of the Ninth Conference on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 460–463. Springer-Verlag, 1997.
C. Holzbaur. OFAI CLP(Q,R), Manual, Edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence, Vienna, 1995.
N. Halbwachs, Y-E. Proy, and P. Roumanoff. Verification of Real-time Systems using Linear Relation Analysis. Formal Methods in System Design, 11(2):157–185, 1997.
J. Jaffar and M. J. Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, 19-20:503–582, 1994.
K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Efficient Verification of Real-time Systems: Compact Data Structure and State-space Reduction. In Proceedings of the 18th IEEE Real Time Systems Symposium (RTSS’97), pages 14–24. IEEE Computer Society, 1997.
K. G. Larsen, P. Pettersson, and W. Yi. uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134–152, 1997.
D. Lesens and H. Saidi. Automatic Verification of Parameterized Networks of Processes by Abstraction. In Proceedings of the International Workshop on Verification Infinite State Systems (INFINITY’97), available at the URL http://sunshine.cs.uni-dortmund.de/organization/pastE.html, 1997.
M. J. Maher. Constrained dependencies. In Ugo Montanari, editor, Proceedings of the First International Conference on Principles and Practice of Constraint Programming (CP’95), Lecture Notes in Computer Science, pages 170–185, Cassis, France, 19-22 September 1995. Springer-Verlag.
K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
M. J. Maher and R. Ramakrishnan. Déjà Vu in Fixpoints of Logic Programs. In Ross A. Lusk and Ewing L. Overbeek, editors, Proceedings of the North American Conference on Logic Programming (NACLP’89), pages 963–980. MIT Press, 1989.
A. Podelski, editor. Constraint Programming: Basics and Trends, volume 910 of LNCS. Springer-Verlag, 1994.
A. Rauzy. Toupie: A Constraint Language for Model Checking. In Podelski [Pod94], pages 193–208.
P. Z. Revesz. A Closed-form Evaluation for Datalog Queries with Integer (Gap)-order Constraints. Theoretical Computer Science, 116(1):117–149, 1993.
Y. S. Ramakrishnan, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient Model Checking using Tabled Resolution. In Orna Grumberg, editor, Proceedings of the Ninth Conference on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 143–154. Springer-Verlag, 1997.
R. Ramakrishnan, D. Srivastava, and S. Sudarshan. Efficient Bottom-up Evaluation of Logic Programs. In P. De Wilde and J. Vandewalle, editors, Computer Systems and Software Engineering: State-of-the-Art, chapter 11. Kluwer Academic, 1992.
U. A. Shankar. An Introduction to Assertional Reasoning for Concurrent Systems. ACM Computing Surveys, 25(3):225–262, 1993.
T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A Comparison of Presburger Engines for EFSM Reachability. In Alan J. Hu and Moshe Y. Vardi, editors, Proceedings of the Tenth Conference on Computer Aided Verification (CAV’98), volume 1427 of LNCS, pages 280–292. Springer-Verlag, 1998.
D. Srivastava. Subsumption and Indexing in Constraint Query Languages with Linear Arithmetic Constraints. Annals of Mathematics and Artificial Intelligence, 8(3-4):315–343, 1993.
H. B. Sipma, T. E. Uribe, and Z. Manna. Deductive Model Checking. In R. Alur and T. Henzinger, editors, Proceedings of the Eighth Conference on Computer Aided Verification (CAV’96), volume 1102 of LNCS, pages 208–219. Springer-Verlag, 1996.
L. Urbina. Analysis of Hybrid Systems in CLP(R). In Eugene C. Freuder, editor, Proceedings of Principles and Practice of Constraint Programming (CP’96), volume 1118 of LNCS, pages 451–467. Springer-Verlag, 1996.
M. Wallace. Practical Applications of Constraint Programming. Constraints, 1(1-2):139–168, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delzanno, G., Podelski, A. (1999). Model Checking in CLP. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49059-0_16
Download citation
DOI: https://doi.org/10.1007/3-540-49059-0_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65703-3
Online ISBN: 978-3-540-49059-3
eBook Packages: Springer Book Archive