{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T06:33:26Z","timestamp":1794378806508,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"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_46","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:36:09Z","timestamp":1278614169000},"page":"543-557","source":"Crossref","is-referenced-by-count":7,"title":["A Dash of Fairness for Compositional Reasoning"],"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":"46_CR1","unstructured":"Alur, R., Henzinger, T.: Reactive modules. In: IEEE LICS (1996)"},{"issue":"2","key":"46_CR2","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput.\u00a075(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"46_CR3","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)"},{"key":"46_CR4","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":"46_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a08(2) (1986)","DOI":"10.1145\/5397.5399"},{"key":"46_CR6","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":"46_CR7","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":"46_CR8","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":"46_CR9","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":"46_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1007\/978-3-642-14295-6_47","volume-title":"CAV 2010","author":"A. Cohen","year":"2010","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y.: SPLIT: A Compositional Ltl Verifier. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 558\u2013561. Springer, Heidelberg (2010)"},{"key":"46_CR11","unstructured":"de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, Cambridge (2001)"},{"key":"46_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)"},{"key":"46_CR13","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: LICS (1986)"},{"key":"46_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time logic strikes back. Sci. of Comp. Programming\u00a08(3) (1987)","DOI":"10.1016\/0167-6423(87)90036-0"},{"key":"46_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-78800-3_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Farzan","year":"2008","unstructured":"Farzan, A., Chen, Y., Clarke, E.M., Tsan, Y., Wang, B.: Extending\u00a0automated\u00a0compositional\u00a0verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 2\u201317. Springer, Heidelberg (2008)"},{"key":"46_CR16","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":"46_CR17","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"},{"issue":"8","key":"46_CR18","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. ACM Commun.\u00a017(8), 453\u2013455 (1974)","journal-title":"ACM Commun."},{"key":"46_CR19","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng.\u00a03(2) (1977)","DOI":"10.1109\/TSE.1977.229904"},{"key":"46_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1997","unstructured":"McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 24\u201335. Springer, Heidelberg (1997)"},{"key":"46_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 342\u2013346. Springer, Heidelberg (1999)"},{"key":"46_CR22","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)"},{"key":"46_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/10722167_14","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 139\u2013153. Springer, Heidelberg (2000)"},{"issue":"5","key":"46_CR24","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":"46_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-78163-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Pnueli","year":"2008","unstructured":"Pnueli, A., Sa\u2019ar, Y.: All you need is compassion. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 233\u2013247. Springer, Heidelberg (2008)"},{"key":"46_CR26","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\/"},{"key":"46_CR27","doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M.B., Pasareanu, C.S.: Automated environment generation for software model checking. In: ASE, pp. 116\u2013129 (2003)","DOI":"10.1109\/ASE.2003.1240300"}],"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_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T14:48:50Z","timestamp":1740235730000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_46","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]]}}}