{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T20:20:32Z","timestamp":1791058832847,"version":"4.1.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,12,11]],"date-time":"2008-12-11T00:00:00Z","timestamp":1228953600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10703-008-0063-8","type":"journal-article","created":{"date-parts":[[2008,12,10]],"date-time":"2008-12-10T14:34:46Z","timestamp":1228919686000},"page":"104-125","source":"Crossref","is-referenced-by-count":25,"title":["Local proofs for global safety properties"],"prefix":"10.1007","volume":"34","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"}]}],"member":"297","published-online":{"date-parts":[[2008,12,11]]},"reference":[{"key":"63_CR1","series-title":"LNCS","first-page":"408","volume-title":"CAV","author":"I Balaban","year":"2005","unstructured":"Balaban I, Fang Y, Pnueli A, Zuck LD (2005) IIV: An invisible invariant verifier. In: CAV. LNCS, vol 3576. Springer, Berlin, pp 408\u2013412"},{"key":"63_CR2","series-title":"LNCS","first-page":"534","volume-title":"CAV","author":"S Chaki","year":"2005","unstructured":"Chaki S, Clarke EM, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: CAV. LNCS, vol 3576. Springer, Berlin, pp 534\u2013547"},{"issue":"4","key":"63_CR3","first-page":"417","volume":"7","author":"KM Chandy","year":"1981","unstructured":"Chandy KM, Misra J (1981) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417\u2013426","journal-title":"IEEE Trans Softw Eng"},{"key":"63_CR4","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O (1987) Avoiding the state explosion problem in temporal logic model checking. In: PODC, pp 294\u2013303","DOI":"10.1145\/41840.41865"},{"issue":"5","key":"63_CR5","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J Assoc Comput Mach 50(5):752\u2013794","journal-title":"J Assoc Comput Mach"},{"key":"63_CR6","series-title":"LNCS","volume-title":"Workshop on logics of programs","author":"EM Clarke","year":"1981","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on logics of programs. LNCS, vol 131. Springer, Berlin"},{"key":"63_CR7","doi-asserted-by":"crossref","unstructured":"Cobleigh JM, Avrunin GS, Clarke LA (2006) Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: ISSTA, pp\u00a097\u2013108","DOI":"10.1145\/1146238.1146250"},{"key":"63_CR8","doi-asserted-by":"crossref","unstructured":"Cohen A, Namjoshi KS (2008) Local proofs for linear-time properties of concurrent programs. In: CAV (to appear)","DOI":"10.1007\/978-3-540-70545-1_15"},{"key":"63_CR9","first-page":"243","volume-title":"Automatic program construction techniques","author":"P Cousot","year":"1984","unstructured":"Cousot P, Cousot R (1984) Invariance proof methods and analysis techniques for parallel programs. In: Biermann AW, Guiho G, Kadratoff Y (eds) Automatic program construction techniques. Macmillan, New York, pp\u00a0243\u2013271, chap\u00a012"},{"key":"63_CR10","volume-title":"Concurrency verification: introduction to compositional and noncompositional proof methods","author":"W-P Roever de","year":"2001","unstructured":"de Roever W-P, de Boer F, Hannemann U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency verification: introduction to compositional and noncompositional proof methods. Cambridge University Press, Cambridge"},{"key":"63_CR11","volume-title":"A discipline of programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra EW (1976) A discipline of programming. Prentice Hall, New York"},{"key":"63_CR12","unstructured":"Dijkstra EW (1976) EWD 554: A Personal Summary of the Gries-Owicki Theory. Available at http:\/\/www.cs.utexas.edu\/users\/EWD"},{"key":"63_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate calculus and program semantics","author":"EW Dijkstra","year":"1990","unstructured":"Dijkstra EW, Scholten CS (1990) Predicate calculus and program semantics. Springer, Berlin"},{"issue":"1\u20133","key":"63_CR14","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/j.tcs.2004.12.006","volume":"338","author":"C Flanagan","year":"2005","unstructured":"Flanagan C, Freund SN, Qadeer S, Seshia SA (2005) Modular verification of multithreaded programs. Theor Comput Sci 338(1\u20133):153\u2013183","journal-title":"Theor Comput Sci"},{"key":"63_CR15","series-title":"LNCS","first-page":"213","volume-title":"SPIN","author":"C Flanagan","year":"2003","unstructured":"Flanagan C, Qadeer S (2003) Thread-modular model checking. In: SPIN. LNCS, vol 2648. Springer, Berlin, pp 213\u2013224"},{"key":"63_CR16","series-title":"LNCS","first-page":"282","volume-title":"SPIN","author":"D Giannakopoulou","year":"2005","unstructured":"Giannakopoulou D, Pasareanu CS (2005) Learning-based assume-guarantee verification (tool paper). In: SPIN. LNCS, vol 3639. Springer, Berlin, pp 282\u2013287"},{"key":"63_CR17","doi-asserted-by":"crossref","unstructured":"Giannakopoulou D, Pasareanu CS, Barringer H (2002) Assumption generation for software component verification. In: ASE, pp\u00a03\u201312","DOI":"10.1109\/ASE.2002.1114984"},{"key":"63_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R (2004) Race checking by context inference. In: PLDI, pp 1\u201313","DOI":"10.1145\/996841.996844"},{"key":"63_CR19","series-title":"LNCS","first-page":"262","volume-title":"CAV","author":"TA Henzinger","year":"2003","unstructured":"Henzinger TA, Jhala R, Majumdar R, Qadeer S (2003) Thread-modular abstraction refinement. In: CAV. LNCS, vol 2725. Springer, Berlin, pp 262\u2013274"},{"key":"63_CR20","series-title":"LNCS","first-page":"3","volume-title":"CAV","author":"AJ Hu","year":"1993","unstructured":"Hu AJ, Dill DL (1993) Efficient verification with bdds using implicitly conjoined invariants. In: CAV. LNCS, vol 697. Springer, Berlin, pp 3\u201314"},{"key":"63_CR21","series-title":"LNCS","first-page":"396","volume-title":"CAV","author":"R Jhala","year":"2001","unstructured":"Jhala R, McMillan KL (2001) Microarchitecture verification by compositional model checking. In: CAV. LNCS, vol 2102. Springer, Berlin, pp 396\u2013410"},{"key":"63_CR22","unstructured":"Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis, Oxford University"},{"issue":"2","key":"63_CR23","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125\u2013143","journal-title":"IEEE Trans Softw Eng"},{"key":"63_CR24","doi-asserted-by":"crossref","unstructured":"Malkis A, Podelski A, Rybalchenko A (2007) Precise thread-modular verification. In: SAS, pp\u00a0218\u2013232","DOI":"10.1007\/978-3-540-74061-2_14"},{"key":"63_CR25","series-title":"LNCS","volume-title":"CAV","author":"KL McMillan","year":"1997","unstructured":"McMillan KL (1997) A compositional rule for hardware design refinement. In: CAV. LNCS, vol 1254. Springer, Berlin"},{"key":"63_CR26","series-title":"LNCS","volume-title":"VMCAI","author":"KS Namjoshi","year":"2007","unstructured":"Namjoshi KS (2007) Symmetry and completeness in the analysis of parameterized systems. In: VMCAI. LNCS, vol 4349. Springer, Berlin"},{"issue":"5","key":"63_CR27","first-page":"279","volume":"19","author":"SS Owicki","year":"1976","unstructured":"Owicki SS, Gries D (1976) Verifying properties of parallel programs: An axiomatic approach. Commun Assoc Comput Mach 19(5):279\u2013285","journal-title":"Commun Assoc Comput Mach"},{"key":"63_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli A (1985) In transition from global to modular reasoning about programs. In: Logics and models of concurrent systems. NATO ASI series","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"63_CR29","series-title":"LNCS","first-page":"82","volume-title":"TACAS","author":"A Pnueli","year":"2001","unstructured":"Pnueli A, Ruah S, Zuck LD (2001) Automatic deductive verification with invisible invariants. In: TACAS. LNCS, vol 2031. Springer, Berlin, pp 82\u201397"},{"key":"63_CR30","series-title":"LNCS","first-page":"184","volume-title":"CAV","author":"A Pnueli","year":"1996","unstructured":"Pnueli A, Shahar E (1996) A platform for combining deductive with algorithmic verification. In: CAV. LNCS, vol 1102. Springer, Berlin, pp 184\u2013195. Web: www.cs.nyu.edu\/acsys\/tlv"},{"key":"63_CR31","series-title":"LNCS","volume-title":"Proc of the 5th international symposium on programming","author":"JP Queille","year":"1982","unstructured":"Queille JP, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: Proc of the 5th international symposium on programming. LNCS, vol 137. Springer, Berlin"},{"key":"63_CR32","doi-asserted-by":"crossref","unstructured":"Shoham S, Grumberg O (2007) Compositional verification and 3-valued abstractions join forces. In: SAS, pp 69\u201386","DOI":"10.1007\/978-3-540-74061-2_5"},{"key":"63_CR33","doi-asserted-by":"crossref","unstructured":"Tkachuk O, Dwyer MB, Pasareanu CS (2003) Automated environment generation for software model checking. In: ASE, pp 116\u2013129","DOI":"10.1109\/ASE.2003.1240300"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0063-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-008-0063-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0063-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:03Z","timestamp":1559253663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-008-0063-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12,11]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["63"],"URL":"https:\/\/doi.org\/10.1007\/s10703-008-0063-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12,11]]}}}