{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:12:16Z","timestamp":1791299536646,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540740605","type":"print"},{"value":"9783540740612","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74061-2_15","type":"book-chapter","created":{"date-parts":[[2007,8,21]],"date-time":"2007-08-21T15:39:13Z","timestamp":1187710753000},"page":"233-248","source":"Crossref","is-referenced-by-count":39,"title":["Modular Safety Checking for Fine-Grained Concurrency"],"prefix":"10.1007","author":[{"given":"Cristiano","family":"Calcagno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Parkinson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/b98229","volume-title":"CONCUR 2004 - Concurrency Theory","author":"T. Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Xie, Y.: Zing: Exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, Springer, Heidelberg (2004)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b105887","volume-title":"APLAS 2005","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, Springer, Heidelberg (2005)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Automatic modular assertion checking with separation logic. In: 4th FMCO, pp. 115\u2013137 (2006)","DOI":"10.1007\/11804192_6"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-540-28644-8_2","volume-title":"CONCUR 2004 - Concurrency Theory","author":"S.D. Brookes","year":"2004","unstructured":"Brookes, S.D.: A semantics for concurrent separation logic (Extended version to appear in Theoretical Computer Science). In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 16\u201334. Springer, Heidelberg (2004)"},{"key":"15_CR6","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_44","volume-title":"Computer Aided Verification","author":"R. Colvin","year":"2006","unstructured":"Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"TACAS 2006 and ETAPS 2006","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"issue":"1-3","key":"15_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":"15_CR10","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI, New York, USA, pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: SPIN (2003)","DOI":"10.1007\/3-540-44829-2_14"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Heller, S., Herlihy, M., Luchangco, V., Moir, M., Scherer, B., Shavit, N.: A lazy concurrent list-based set algorithm. In: 9th OPODIS (December 2005)","DOI":"10.1007\/11795490_3"},{"key":"15_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":"15_CR15","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Conference (1983)"},{"issue":"7","key":"15_CR16","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"3","key":"15_CR17","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/44501.44503","volume":"10","author":"C. Morgan","year":"1988","unstructured":"Morgan, C.: The specification statement. ACM Trans. Program. Lang. Sys.\u00a010(3), 403\u2013419 (1988)","journal-title":"ACM Trans. Program. Lang. Sys."},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","first-page":"271","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 271\u2013307. Springer, Heidelberg (2004)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: 31st POPL, pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"issue":"5","key":"15_CR20","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Comm. ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Comm. ACM"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bornat, R., O\u2019Hearn, P.: Modular verification of a non-blocking stack. In: 34th POPL (2007)","DOI":"10.1145\/1190216.1190261"},{"issue":"3","key":"15_CR22","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett.\u00a012(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"15_CR23","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science\u00a013(1), 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"15_CR24","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/982962.964022","volume":"39","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Rajamani, S.K., Rehof, J.: Summarizing procedures in concurrent programs. SIGPLAN Not.\u00a039(1), 245\u2013255 (2004)","journal-title":"SIGPLAN Not."},{"key":"15_CR25","first-page":"55","volume-title":"17th LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"issue":"1","key":"15_CR26","first-page":"17","volume":"137","author":"H. Simpson","year":"1990","unstructured":"Simpson, H.: Four-slot fully asynchronous communication mechanism. IEE Proceedings\u00a0137(1), 17\u201330 (1990)","journal-title":"IEE Proceedings"},{"key":"15_CR27","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/1122971.1122992","volume-title":"11th PPoPP","author":"V. Vafeiadis","year":"2006","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: 11th PPoPP, pp. 129\u2013136. ACM Press, New York (2006)"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: 18th CONCUR (2007)","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci.\u00a089(3) (2003)","DOI":"10.1016\/S1571-0661(05)80006-4"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74061-2_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T21:21:31Z","timestamp":1684012891000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74061-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540740605","9783540740612"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74061-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}