{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T06:10:09Z","timestamp":1737094209275,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008972"},{"type":"electronic","value":"9783540365761"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/3-540-36576-1_22","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T02:42:17Z","timestamp":1181616137000},"page":"343-357","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Compositional Circular Assume-Guarantee Rules Cannot Be Sound and Complete"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Maier","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"issue":"3","key":"22_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507\u2013534, 1995.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60246-1_155","volume-title":"MFCS","author":"M. Abadi","year":"1995","unstructured":"M. Abadi and S. Merz. An abstract account of composition. In MFCS, LNCS 969, pages 499\u2013508. Springer, 1995."},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181\u2013185, 1985.","journal-title":"Information Processing Letters"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur and T. A. Henzinger. Reactive modules. In LICS, pages 207\u2013218. IEEE Computer Society, 1996.","DOI":"10.1109\/LICS.1996.561320"},{"key":"22_CR5","unstructured":"E. A. Emerson. Modal and temporal logics. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 135\u2013191. Elsevier, 1990."},{"key":"22_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/3-540-45927-8_19","volume-title":"ESOP","author":"C. Flangan","year":"2002","unstructured":"C. Flangan, S. N. Freund, and S. Qadeer. Thread-modular verification for sharedmemory programs. In ESOP, LNCS 2305, pages 262\u2013277. Springer, 2002."},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, X. Liu, S. Qadeer, and S. K. Rajamani. Formal specification and verification of a dataflow processor array. In ICCAD, pages 494\u2013499. IEEE Computer Society, 1999.","DOI":"10.1109\/ICCAD.1999.810700"},{"key":"22_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/BFb0028765","volume-title":"CAV","author":"T. A. Henzinger","year":"1998","unstructured":"T. A. Henzinger, S. Qadeer, and S. K. Rajamani. You assume, we guarantee: Methodology and case studies. In CAV, LNCS 1427, pages 440\u2013451. Springer, 1998."},{"issue":"1","key":"22_CR9","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/509705.509707","volume":"24","author":"T. A. Henzinger","year":"2002","unstructured":"T. A. Henzinger, S. Qadeer, S. K. Rajamani, and S. Tasiran. An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems, 24(1):51\u201364, 2002.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0304-3975(96)00069-2","volume":"167","author":"B. Jonsson","year":"1996","unstructured":"B. Jonsson and Y.-K. Tsay. Assumption\/guarantee specifications in linear-time temporal logic. Theoretical Computer Science, 167(1\u20132):47\u201372, 1996.","journal-title":"Theoretical Computer Science"},{"key":"22_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1007\/3-540-48224-5_67","volume-title":"ICALP","author":"P. Maier","year":"2001","unstructured":"P. Maier. A set-theoretic framework for assume-guarantee reasoning. In ICALP, LNCS 2076, pages 821\u2013834. Springer, 2001."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"P. Maier. A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning. PhD thesis, Universit\u00e4t des Saarlandes, 2002. Submitted.","DOI":"10.1007\/3-540-48224-5_67"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"P. Maier. Compositional circular assume-guarantee rules cannot be sound and complete. Technical Report MPI-I-2003-2-001, Max-Planck-Institut f\u00fcr Informatik, 2003.","DOI":"10.1007\/3-540-36576-1_22"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"22_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"CAV","author":"K. L. McMillan","year":"1998","unstructured":"K. L. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In CAV, LNCS 1427, pages 110\u2013121. Springer, 1998."},{"key":"22_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"CHARME","author":"K. L. McMillan","year":"1999","unstructured":"K. L. McMillan. Circular compositional reasoning about liveness. In CHARME, LNCS 1703, pages 342\u2013345. Springer, 1999."},{"issue":"4","key":"22_CR17","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"J. Misra and K. M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(4):417\u2013426, 1981.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/10722167_14","volume-title":"CAV","author":"K. S. Namjoshi","year":"2000","unstructured":"K. S. Namjoshi and R. J. Trefler. On the completeness of compositional reasoning. In CAV, LNCS 1855, pages 139\u2013153. Springer, 2000."},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 135\u2013191. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"22_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"835","DOI":"10.1007\/3-540-48224-5_68","volume-title":"ICALP","author":"M. Viswanathan","year":"2001","unstructured":"M. Viswanathan and R. Viswanathan. Foundations for circular compositional reasoning. In ICALP, LNCS 2076, pages 835\u2013847. Springer, 2001."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36576-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:53:48Z","timestamp":1737093228000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36576-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008972","9783540365761"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-36576-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}