{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:57:14Z","timestamp":1725490634634},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_9","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"55-67","source":"Crossref","is-referenced-by-count":18,"title":["Local Proofs for Global Safety Properties"],"prefix":"10.1007","author":[{"given":"Ariel","family":"Cohen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"534","DOI":"10.1007\/11513988_51","volume-title":"Computer Aided Verification","author":"S. Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E.M., Sinha, N., Thati, P.: Automated assume-guarantee reasoning for simulation conformance. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 534\u2013547. Springer, Heidelberg (2005)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering\u00a07 (1981)","DOI":"10.1109\/TSE.1981.230844"},{"key":"9_CR3","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"},{"issue":"5","key":"9_CR4","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, Springer, Heidelberg (1982)"},{"key":"9_CR6","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":"9_CR7","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods","author":"W-P.d. Roever","year":"2001","unstructured":"Roever, W-P.d., Boer, F.d., 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":"9_CR8","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)"},{"issue":"1-3","key":"9_CR9","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.tcs.2004.12.006","volume":"338","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci.\u00a0338(1-3), 153\u2013183 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR10","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.) Model Checking Software. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"9_CR11","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.) Model Checking Software. LNCS, vol.\u00a03639, pp. 282\u2013287. Springer, Heidelberg (2005)"},{"key":"9_CR12","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":"9_CR13","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI, pp. 1\u201313 (2004)","DOI":"10.1145\/996841.996844"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 262\u2013274. Springer, Heidelberg (2003)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","first-page":"3","volume-title":"Computer Aided Verification","author":"A.J. Hu","year":"1993","unstructured":"Hu, A.J., Dill, D.L.: Efficient verification with BDDs using implicitly conjoined invariants. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 3\u201314. Springer, Heidelberg (1993)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2001","unstructured":"Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 396\u2013410. Springer, Heidelberg (2001)"},{"key":"9_CR17","unstructured":"Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University (1981)"},{"key":"9_CR18","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":"9_CR19","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (1997)"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-75596-8","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, Springer, Heidelberg (2007)"},{"issue":"5","key":"9_CR21","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. Commun. ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 184\u2013195. Springer, Heidelberg (1996), web: www.cs.nyu.edu\/acsys\/tlv"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol.\u00a0137, Springer, Heidelberg (1982)"},{"key":"9_CR25","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-540-73368-3_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:42Z","timestamp":1619518122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_9","relation":{},"subject":[]}}