{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T14:52:13Z","timestamp":1772549533786,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540665595","type":"print"},{"value":"9783540481539","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_30","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"342-346","source":"Crossref","is-referenced-by-count":57,"title":["Circular Compositional Reasoning about Liveness"],"prefix":"10.1007","author":[{"given":"K. L.","family":"McMillan","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"30_CR1","unstructured":"http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/papers\/1999-02.ps.gz\n                    \n                  ,Feb. 1999."},{"issue":"1","key":"30_CR2","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Trans.on Prog.Lang. and Syst., 15(1):73\u2013132,Jan. 1993.","journal-title":"ACM Trans.on Prog.Lang. and Syst."},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur and T. A. Henzinger. Reactive modules. In 11th annual IEEE symp. Logic in Computer Science (LICS\u2019 96), 1996.","DOI":"10.1109\/LICS.1996.561320"},{"key":"30_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"CAV\u2019 98","author":"R. Alur","year":"1998","unstructured":"R. Alur, T. A. Henzinger, F. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. Mocha:Modularity in model checking.In CAV\u2019 98, number 1427 LNCS, pages 521\u2013525. Springer-Verlag."},{"key":"30_CR5","unstructured":"L. Lamport. The temporal logic of actions. Research report 79,Digital Equipment Corporation, Systems Research Center, Dec. 1991."},{"key":"30_CR6","unstructured":"K. L. McMillan. Verification of infinite state systems by compositional model checking. this volume."},{"key":"30_CR7","series-title":"Lect Notes Comput Sci","first-page":"100","volume-title":"CAV\u201998","author":"K. L. McMillan","year":"1998","unstructured":"K. L. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In CAV\u201998,number 1427 in LNCS,pages 100\u2013121. Springer-Verlag, 1998."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T14:21:49Z","timestamp":1551104509000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}