{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T06:33:27Z","timestamp":1794378807272,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142949","type":"print"},{"value":"9783642142956","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_47","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:36:09Z","timestamp":1278614169000},"page":"558-561","source":"Crossref","is-referenced-by-count":8,"title":["SPLIT: A Compositional LTL Verifier"],"prefix":"10.1007","author":[{"given":"Ariel","family":"Cohen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yaniv","family":"Sa\u2019ar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"47_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"47_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: PODC, pp. 294\u2013303 (1987)","DOI":"10.1145\/41840.41865"},{"key":"47_CR3","doi-asserted-by":"crossref","unstructured":"Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: ISSTA, pp. 97\u2013108 (2006)","DOI":"10.1145\/1146238.1146250"},{"key":"47_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-540-73368-3_9","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2007","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 55\u201367. Springer, Heidelberg (2007)"},{"key":"47_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-70545-1_15","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2008","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for linear-time properties of concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 149\u2013161. Springer, Heidelberg (2008)"},{"key":"47_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/978-3-642-14295-6_46","volume-title":"CAV 2010","author":"A. Cohen","year":"2010","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y.: A dash of fairness for compositional reasoning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 543\u2013557. Springer, Heidelberg (2010)"},{"key":"47_CR7","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y., Zuck, L.D.: Symbolic model checking on multi-core processors. Technical report, Bell Laboratories (2009)"},{"key":"47_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"47_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1007\/11537328_24","volume-title":"Model Checking Software","author":"D. Giannakopoulou","year":"2005","unstructured":"Giannakopoulou, D., Pasareanu, C.S.: Learning-based assume-guarantee verification (tool paper). In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 282\u2013287. Springer, Heidelberg (2005)"},{"key":"47_CR10","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption generation for software component verification. In: ASE, pp. 3\u201312 (2002)","DOI":"10.1109\/ASE.2002.1114984"},{"key":"47_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"47_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-69738-1_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.S. Namjoshi","year":"2007","unstructured":"Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 299\u2013313. Springer, Heidelberg (2007)"},{"issue":"5","key":"47_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. ACM Commun.\u00a019(5), 279\u2013285 (1976)","journal-title":"ACM Commun."},{"key":"47_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-14295-6_18","volume-title":"CAV 2010","author":"A. Pnueli","year":"2010","unstructured":"Pnueli, A., Sa\u2019ar, Y., Zuck, L.D.: Jtlv: A framework for developing verification algorithms. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 171\u2013174. Springer, Heidelberg (2010), http:\/\/jtlv.ysaar.net\/"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T14:48:54Z","timestamp":1740235734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_47","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}