{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:02:35Z","timestamp":1767337355215},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_26","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T05:24:41Z","timestamp":1180675481000},"page":"384-398","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Constraint Logic Programming for Local and Symbolic Model-Checking"],"prefix":"10.1007","author":[{"given":"Ulf","family":"Nilsson","sequence":"first","affiliation":[]},{"given":"Johan","family":"L\u00fcbcke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0743-1066(94)90024-8","volume":"19\/20","author":"K. Apt","year":"1994","unstructured":"K. Apt and R. Bol. Logic Programming and Negation: A Survey. J. Logic Programming, 19\/20:9\u201371, 1994.","journal-title":"J. Logic Programming"},{"issue":"4","key":"26_CR2","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch, E. M. Clarke, D. E. Long, K. I. McMillan, and D. L. Dill. Symbolic Model Checking for Sequential Circuit Verification. IEEE Trans on Computer-Aided Design of Integrated Circuits, 13(4):401\u2013424, 1994.","journal-title":"IEEE Trans on Computer-Aided Design of Integrated Circuits"},{"key":"26_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/BFb0054183","volume-title":"Proc. of TACAS\u201998","author":"W. Charatonik","year":"1998","unstructured":"W. Charatonik and A. Podelski. Set-Based Analysis of Reactive Infinite-State Systems. In Proc. of TACAS\u201998, Lecture Notes in Computer Science 1384, pages 358\u2013375. Springer-Verlag, 1998."},{"issue":"1","key":"26_CR4","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/227595.227597","volume":"43","author":"W. Chen","year":"1996","unstructured":"W. Chen and D. S. Warren. Tabled Evaluation With Delaying for General Logic Programs. J. ACM, 43(1):20\u201374, 1996.","journal-title":"J. ACM"},{"key":"26_CR5","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000."},{"key":"26_CR6","unstructured":"L. Degerstedt. Tabulation-based Logic Programming. PhD thesis, Link\u00f6ping studies in Science and Technology, dissertation no 462, 1996."},{"key":"26_CR7","unstructured":"G. Delzanno and A. Podelski. Model Checking Infinite-State Systems using CLP. Technical report MPI-I-98-2-012, Max-Planck-Institut f\u00fcr Informatik, 1998."},{"key":"26_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Proc of TACAS\u201999, Amsterdam","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model Checking in CLP. In Proc of TACAS\u201999, Amsterdam, Lecture Notes in Computer Science 1579. Springer Verlag, 1999."},{"key":"26_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc of TACAS\u201999, Amsterdam","author":"Y. Dong","year":"1999","unstructured":"Y. Dong, X. Du, Y. Ramakrishna, I. Ramakrishnan, S. Smolka, O. Sokolsky, E. Stark, and D. Warren. Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools. In Proc of TACAS\u201999, Amsterdam, Lecture Notes in Computer Science 1579. Springer Verlag, 1999."},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and Modal Logics. In Jan van Leeuwen, editor, Handbook on Theoretical Computer Science, volume B, pages 995\u20131072. Elsevier Science, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"26_CR11","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991."},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"J. Jaffar and J-L. Lassez. Constraint Logic Programming. In Conf. Record of 14th Annual ACM Symp. on POPL, pages 111\u2013119, 1987.","DOI":"10.1145\/41625.41635"},{"key":"26_CR13","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. Maher. Constraint Logic Programming: A Survey. J. Logic Programming, 19\/20:503\u2013581, 1994.","journal-title":"J. Logic Programming"},{"key":"26_CR14","unstructured":"J. L\u00fcbcke and U. Nilsson. On-the-fly CTL Model-checking using Constraint Logic Programming. In Intl Workshop on Constraint Programming for Time-Critical Applications, COTIC99, 1999."},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"26_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proc of Computer Aided Verification (CAV)","author":"Y. S. Ramakrishna","year":"1997","unstructured":"Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. Smolka, T. Swift, and D. S. Warren. Efficient Model Checking using Tabled Resolution. In Proc of Computer Aided Verification (CAV), Lecture Notes in Computer Science 1254. Springer Verlag, 1997."},{"key":"26_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-60045-0_44","volume-title":"Proc. of Computer Aided Verification 1995","author":"A. Rauzy","year":"1995","unstructured":"A. Rauzy. Toupie = Mu-calculus + Constraints. In Proc. of Computer Aided Verification 1995, Lecture Notes in Computer Science 939, pages 114\u2013126. Springer Verlag, 1995."},{"key":"26_CR18","unstructured":"K. Sagonaset al. The XSB Programmer\u2019s Manual Version 2.0, 1999."},{"issue":"1","key":"26_CR19","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C. Stirling","year":"1991","unstructured":"C. Stirling and D. Walker. Local Model Checking in the Modal Mu-calculus. Theoretical Computer Science, 89(1):161\u2013177, 1991.","journal-title":"Theoretical Computer Science"},{"key":"26_CR20","unstructured":"P. Stuckey. Constructive Negation for Constraint Logic Programming. In Proc of Logic in Computer Science (LICS\u201991), 1991."},{"key":"26_CR21","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1023\/A:1009799613661","volume":"2","author":"D. Toman","year":"1997","unstructured":"D. Toman. Memoing Evaluation for Constraint Extensions of Datalog. J. Constraints, 2:337\u2013359, 1997.","journal-title":"J. Constraints"},{"issue":"3","key":"26_CR22","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/131295.131299","volume":"35","author":"D.S. Warren","year":"1992","unstructured":"D.S. Warren. Memoing for Logic Programs. CACM, 35(3):93\u2013111, 1992.","journal-title":"CACM"}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:31:18Z","timestamp":1558272678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"15 December 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}