{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:23:20Z","timestamp":1778300600810,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540657033","type":"print"},{"value":"9783540490593","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49059-0_16","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T21:56:57Z","timestamp":1194991017000},"page":"223-239","source":"Crossref","is-referenced-by-count":86,"title":["Model Checking in CLP"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,3,12]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. \u010cer\u0101ns, 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\u201996), pages 313\u2013321. IEEE Computer Society Press, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"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\u201990), pages 428\u2013439. IEEE Society Press, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"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\u201998), pages 113\u2013123. ACM Press, 1998.","DOI":"10.1145\/271771.271799"},{"key":"16_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Proceedings of the Ninth Conference on Computer Aided Verification (CAV\u201997)","author":"T. Bultan","year":"1997","unstructured":"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\u201997), volume 1254 of LNCS, pages 400\u2013411. Springer-Verlag, 1997."},{"key":"16_CR5","series-title":"Technical Report","volume-title":"Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results","author":"T. Bultan","year":"1998","unstructured":"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."},{"key":"16_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Proceedings of the Sixth International Conference on Computer Aided Verification (CAV\u201994)","author":"B. Boigelot","year":"1994","unstructured":"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\u201994), volume 818 of LNCS, pages 55\u201367. Springer-Verlag, 1994."},{"key":"16_CR7","series-title":"Lect Notes Comput Sci","first-page":"88","volume-title":"Proceedings of the Tenth Conference on Computer Aided Verification (CAV\u201998)","author":"B. Boigelot","year":"1998","unstructured":"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\u201998), volume 1427 of LNCS, pages 88\u201397. Springer-Verlag, 1998."},{"key":"16_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-63166-6_32","volume-title":"Proceedings of the Ninth Conference on Computer Aided Verification (CAV\u201997)","author":"W. Chan","year":"1997","unstructured":"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\u201997), volume 1254 of LNCS, pages 316\u2013327. Springer-Verlag, 1997."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"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\u201978), pages 84\u201396. ACM Press, 1978.","DOI":"10.1145\/512760.512770"},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Proceedings of the Tenth Conference on Computer Aided Verification (CAV\u201998)","author":"H. Comon","year":"1998","unstructured":"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\u201998), volume 1427 of LNCS, pages 268\u2013279. Springer-Verlag, 1998."},{"key":"16_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/BFb0054183","volume-title":"Proceedings of of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998)","author":"W. Charatonik","year":"1998","unstructured":"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\u201998), volume 1384 of LNCS, pages 358\u2013375. Springer-Verlag, 1998."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and Modal Logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995\u20131072. Elsevier Science, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"3-4","key":"16_CR13","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1023\/A:1009747629591","volume":"2","author":"L. Fribourg","year":"1997","unstructured":"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\u2013336, 1997.","journal-title":"Journal of Constraints"},{"key":"16_CR14","unstructured":"L. Fribourg and J. Richardson. Symbolic Verification with Gap-order Constraints. Technical Report LIENS-93-3, Laboratoire d\u2019Informatique, Ecole Normale Superieure, Paris, 1996."},{"issue":"5","key":"16_CR15","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1093\/logcom\/5.2.133","volume":"2","author":"M. Gabbrielli","year":"1995","unstructured":"M. Gabbrielli, M. G. Dore, and G. Levi. Observable Semantics for Constraint Logic Programs. Journal of Logic and Computation, 2(5):133\u2013171, 1995.","journal-title":"Journal of Logic and Computation"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"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\u201997). IEEE Computer Society, 1997.","DOI":"10.1109\/REAL.1997.641285"},{"key":"16_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Proceedings of the Ninth Conference on Computer Aided Verification (CAV\u201997)","author":"T. A. Henzinger","year":"1997","unstructured":"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\u201997), volume 1254 of LNCS, pages 460\u2013463. Springer-Verlag, 1997."},{"key":"16_CR18","unstructured":"C. Holzbaur. OFAI CLP(Q,R), Manual, Edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence, Vienna, 1995."},{"issue":"2","key":"16_CR19","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"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\u2013185, 1997.","journal-title":"Formal Methods in System Design"},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19-20","author":"J. Jaffar","year":"1994","unstructured":"J. Jaffar and M. J. Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, 19-20:503\u2013582, 1994.","journal-title":"Journal of Logic Programming"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"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\u201997), pages 14\u201324. IEEE Computer Society, 1997.","DOI":"10.1109\/REAL.1997.641265"},{"issue":"1-2","key":"16_CR22","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134\u2013152, 1997.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"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\u201997), available at the URL http:\/\/sunshine.cs.uni-dortmund.de\/organization\/pastE.html , 1997.","DOI":"10.1145\/263699.263747"},{"key":"16_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1007\/3-540-60299-2_11","volume-title":"Proceedings of the First International Conference on Principles and Practice of Constraint Programming (CP\u201995)","author":"M. J. Maher","year":"1995","unstructured":"M. J. Maher. Constrained dependencies. In Ugo Montanari, editor, Proceedings of the First International Conference on Principles and Practice of Constraint Programming (CP\u201995), Lecture Notes in Computer Science, pages 170\u2013185, Cassis, France, 19-22 September 1995. Springer-Verlag."},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"16_CR27","unstructured":"M. J. Maher and R. Ramakrishnan. D\u00e9j\u00e0 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\u201989), pages 963\u2013980. MIT Press, 1989."},{"key":"16_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Constraint Programming: Basics and Trends","year":"1994","unstructured":"A. Podelski, editor. Constraint Programming: Basics and Trends, volume 910 of LNCS. Springer-Verlag, 1994."},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"A. Rauzy. Toupie: A Constraint Language for Model Checking. In Podelski [Pod94], pages 193\u2013208.","DOI":"10.1007\/3-540-59155-9_11"},{"issue":"1","key":"16_CR30","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"P. Z. Revesz","year":"1993","unstructured":"P. Z. Revesz. A Closed-form Evaluation for Datalog Queries with Integer (Gap)-order Constraints. Theoretical Computer Science, 116(1):117\u2013149, 1993.","journal-title":"Theoretical Computer Science"},{"key":"16_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"Proceedings of the Ninth Conference on Computer Aided Verification (CAV\u201997)","author":"Y. S. Ramakrishnan","year":"1997","unstructured":"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\u201997), volume 1254 of LNCS, pages 143\u2013154. Springer-Verlag, 1997."},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/978-1-4615-3506-5_11"},{"issue":"3","key":"16_CR33","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/158439.158441","volume":"25","author":"U. A. Shankar","year":"1993","unstructured":"U. A. Shankar. An Introduction to Assertional Reasoning for Concurrent Systems. ACM Computing Surveys, 25(3):225\u2013262, 1993.","journal-title":"ACM Computing Surveys"},{"key":"16_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/BFb0028752","volume-title":"Proceedings of the Tenth Conference on Computer Aided Verification (CAV\u201998)","author":"T. R. Shiple","year":"1998","unstructured":"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\u201998), volume 1427 of LNCS, pages 280\u2013292. Springer-Verlag, 1998."},{"issue":"3-4","key":"16_CR35","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/BF01530796","volume":"8","author":"D. Srivastava","year":"1993","unstructured":"D. Srivastava. Subsumption and Indexing in Constraint Query Languages with Linear Arithmetic Constraints. Annals of Mathematics and Artificial Intelligence, 8(3-4):315\u2013343, 1993.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"16_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/3-540-61474-5_70","volume-title":"Proceedings of the Eighth Conference on Computer Aided Verification (CAV\u201996)","author":"H. B. Sipma","year":"1996","unstructured":"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\u201996), volume 1102 of LNCS, pages 208\u2013219. Springer-Verlag, 1996."},{"key":"16_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/3-540-61551-2_93","volume-title":"Proceedings of Principles and Practice of Constraint Programming (CP\u201996)","author":"L. Urbina","year":"1996","unstructured":"L. Urbina. Analysis of Hybrid Systems in CLP(R). In Eugene C. Freuder, editor, Proceedings of Principles and Practice of Constraint Programming (CP\u201996), volume 1118 of LNCS, pages 451\u2013467. Springer-Verlag, 1996."},{"issue":"1-2","key":"16_CR38","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF00143881","volume":"1","author":"M. Wallace","year":"1996","unstructured":"M. Wallace. Practical Applications of Constraint Programming. Constraints, 1(1-2):139\u2013168, 1996.","journal-title":"Constraints"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49059-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T08:33:49Z","timestamp":1737534829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49059-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657033","9783540490593"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-49059-0_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}