{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:06:41Z","timestamp":1754485601905,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540428633"},{"type":"electronic","value":"9783540455783"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1007\/3-540-45578-7_20","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T06:34:25Z","timestamp":1180334065000},"page":"286-301","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Constraint-Based Verification of Client-Server Protocols"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,11,19]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cer\u0101ns, B. Jonsson and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS\u2019 99, pp. 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"20_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/3-540-45319-9_12","volume-title":"Parameterized Verification of Multithreaded Software Libraries","author":"T. Ball","year":"2001","unstructured":"T. Ball, S. Chaki, S. K. Rajamani. Parameterized Verification of Multithreaded Software Libraries. In Proc. TACAS\u2019 01, LNCS 2031, pp. 158\u2013173, 2001."},{"issue":"4","key":"20_CR3","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM TOPLAS, 21(4):747\u2013789, 1999.","journal-title":"ACM TOPLAS"},{"issue":"1","key":"20_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/332740.332746","volume":"9","author":"T. Bultan","year":"2000","unstructured":"T. Bultan, R. Gerber, C. League Composite model-checking: verification with type-specific symbolic representations.ACM TOSEM, 9(1): 3\u201350, 2000.","journal-title":"ACM TOSEM"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"T. Bultan. Action Language: A specification language for model checking reactive systems. In Proc. ICSE\u2019 00, pp. 335\u2013344, 2000.","DOI":"10.1145\/337180.337219"},{"key":"20_CR6","unstructured":"T. Bultan and T. Yavuz-Kahveci. Action Language Verifier. In Proc. ASE\u2019 01, 2001."},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. POPL\u2019 77 pp. 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"20_CR8","unstructured":"E. M. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press, December 1999."},{"key":"20_CR9","unstructured":"Fabio Somenzi. CUDD: the CU Decision Diagram Package, Release 2.3.1. http:\/\/vlsi.colorado.edu\/~fabio\/cudd\/ ."},{"key":"20_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Automatic Verification of Parameterized Cache Coherence Protocols","author":"G. Delzanno","year":"2000","unstructured":"G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. In Proc. CAV\u2019 00, LNCS 1855, pp. 53\u201368, 1996."},{"key":"20_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-48168-0_5","volume-title":"Constraint-based Analysis of Broadcast Protocols","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno, J. Esparza, and A. Podelski. Constraint-based Analysis of Broadcast Protocols. In Proc. CSL\u2019 99, LNCS 1683, pp. 50\u201366, 1999."},{"key":"20_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Model Checking in CLP","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno, A. Podelski. Model Checking in CLP. In Proc. TACAS\u2019 99, LNCS 1579, pp. 223\u2013239, 1999."},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. On Model Checking for Nondeterministic Infinite-state Systems. In Proc. LICS\u2019 98, pp. 70\u201380, 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS\u2019 99, pp. 352\u2013359, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"20_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/10720327_3","volume-title":"Constraint Logic Programming Applied to Model Checking","author":"L. Fribourg","year":"2000","unstructured":"L. Fribourg. Constraint Logic Programming Applied to Model Checking. In Proc. LOPSTR\u2019 99, LNCS 1817, pp. 30\u201341, 1999."},{"key":"20_CR16","unstructured":"S.M. German. Personal communication."},{"issue":"3","key":"20_CR17","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German, A. P. Sistla. Reasoning about Systems with Many Processes. JACM 39(3): 675\u2013735 (1992)","journal-title":"JACM"},{"key":"20_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Delay Analysis in Synchronous Programs","author":"N. Halbwachs","year":"1993","unstructured":"N. Halbwachs. Delay Analysis in Synchronous Programs. In Proc. CAV\u2019 93, LNCS 697, pp. 333\u2013346, 1993."},{"issue":"2","key":"20_CR19","first-page":"32","volume":"69","author":"G. Holzmann","year":"1988","unstructured":"G. Holzmann Algorithms for Automated Protocol Verification. AT&T Technical Journal 69(2):32\u201344, 1988.","journal-title":"AT&T Technical Journal"},{"key":"20_CR20","unstructured":"W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The Omega library interface guide. Technical Report CS-TR-3445, Department of Computer Science, University of Maryland, College Park, March 1995. See also http:\/\/www.cs.umd.edu\/projects\/omega\/ ."},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In Proc. CAV\u2019 97, pp. 424\u2013435, 1997.","DOI":"10.1007\/3-540-63166-6_41"},{"key":"20_CR22","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":"20_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Automatic Deductive Verification with Invisible Invariants","author":"A. Pnueli","year":"2001","unstructured":"A. Pnueli, S. Ruah, L. D. Zuck Automatic Deductive Verification with Invisible Invariants. In Proc. TACAS\u2019 01, LNCS 2031, pp. 82\u201397, 2001."},{"key":"20_CR24","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. The Omega Test: a Fast and Practical Integer Programming Algorithm for Dependence Analysis. Communications of the ACM, 8:102\u2013114, 1992.","journal-title":"Communications of the ACM"},{"key":"20_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-45319-9_5","volume-title":"A Library for Composite Symbolic Representations","author":"T. Yavuz-Kahveci","year":"2001","unstructured":"T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. A Library for Composite Symbolic Representations. In Proc. TACAS\u2019 01, LNCS 2031, pp. 52\u201366, 2001."}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2014 CP 2001"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45578-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:35:56Z","timestamp":1737052556000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45578-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540428633","9783540455783"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45578-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"19 November 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}