{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:15Z","timestamp":1775790795778,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216676","type":"print"},{"value":"9783319216683","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_26","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T15:08:53Z","timestamp":1436800133000},"page":"449-465","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Automated and Modular Refinement Reasoning for Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Chris","family":"Hawblitzel","sequence":"first","affiliation":[]},{"given":"Erez","family":"Petrank","sequence":"additional","affiliation":[]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"issue":"1","key":"26_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73\u2013132 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"26_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447\u2013466 (2010)","journal-title":"STTT"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Computer Aided Verification, 10th International Conference Proceedings, CAV 1998, pp. 521\u2013525, Vancouver, June 28 - July 2 (1998)","DOI":"10.1007\/BFb0028774"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE (2005)","DOI":"10.1145\/1108792.1108813"},{"issue":"5","key":"26_CR6","doi-asserted-by":"publisher","first-page":"720","DOI":"10.1145\/324133.324234","volume":"46","author":"RD Blumofe","year":"1999","unstructured":"Blumofe, R.D., Leiserson, C.E.: Scheduling multithreaded computations by work stealing. J. ACM 46(5), 720\u2013748 (1999)","journal-title":"J. ACM"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Static Analysis: 10th International Symposium (2003)","DOI":"10.1007\/3-540-44898-5_4"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"11","key":"26_CR10","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/359642.359655","volume":"21","author":"EW Dijkstra","year":"1978","unstructured":"Dijkstra, E.W., Lamport, L., Martin, A.J., Scholten, C.S., Steffens, E.F.M.: On-the-fly garbage collection An exercise in cooperation. Commun. ACM 21(11), 280\u2013294 (1978)","journal-title":"Commun. ACM"},{"issue":"1","key":"26_CR11","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008773308108","volume":"16","author":"AT Eir\u00edksson","year":"2000","unstructured":"Eir\u00edksson, A.T.: The formal design of 1M-gate ASICs. Form. Methods Syst. Des. 16(1), 7\u201322 (2000)","journal-title":"Form. Methods Syst. Des."},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-642-12002-2_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Elmas","year":"2010","unstructured":"Elmas, T., Qadeer, S., Sezgin, A., Subasi, O., Tasiran, S.: Simplifying linearizability proofs with reduction and abstraction. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 296\u2013311. Springer, Heidelberg (2010)"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL, pp. 2\u201315 (2009)","DOI":"10.1145\/1594834.1480885"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Elmas, T., Tasiran, S., Qadeer, S..: VYRD: verifying concurrent programs by runtime refinement-violation detection. In: Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, pp. 27\u201337, Chicago, 12\u201315 June 2005","DOI":"10.1145\/1065010.1065015"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proofs that count. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014), San Diego, pp. 151\u2013164, 20\u201321, January 2014","DOI":"10.1145\/2535838.2535885"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-71316-6_13","volume-title":"Programming Languages and Systems","author":"X Feng","year":"2007","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 173\u2013188. Springer, Heidelberg (2007)"},{"issue":"4","key":"26_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1377492.1377495","volume":"30","author":"C Flanagan","year":"2008","unstructured":"Flanagan, C., Freund, S.N., Lifshin, M., Qadeer, S.: Types for atomicity: Static checking and inference for java. ACM Trans. Program. Lang. Syst. 30(4), 1\u201353 (2008)","journal-title":". ACM Trans. Program. Lang. Syst."},{"issue":"1\u20133","key":"26_CR18","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. 338(1\u20133), 153\u2013183 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR19","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. 2648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning meaning to programs. In: Symposia in Applied Mathematics, vol. 19, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"6","key":"26_CR21","doi-asserted-by":"publisher","first-page":"81","DOI":"10.5381\/jot.2004.3.6.a4","volume":"3","author":"SN Freund","year":"2004","unstructured":"Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. J. Object Technol. 3(6), 81\u2013101 (2004)","journal-title":"J. Object Technol."},{"key":"26_CR22","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Verified concurrent garbage collector. http:\/\/singularity.codeplex.com\/SourceControl\/latest#base\/Imported\/Bartok\/runtime\/verified\/GCs\/concur\/GC.bpl"},{"key":"26_CR23","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. Technical report MSR-TR-2015-8, Microsoft Research (2015). http:\/\/research.microsoft.com\/apps\/pubs\/?id=238907"},{"key":"26_CR24","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: FOCS (1995)"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-40184-8_18","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"TA Henzinger","year":"2013","unstructured":"Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052, pp. 242\u2013256. Springer, Heidelberg (2013)"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Liu, X., Qadeer, S., Rajamani, S.K.: Formal specification and verification of a dataflow processor array. In: Proceedings 1999 IEEE\/ACM International Conference on Computer-aided Design, (ICCAD 1999), pp. 494\u2013499. IEEE Press (1999)","DOI":"10.1109\/ICCAD.1999.810700"},{"key":"26_CR27","volume-title":"The Art of Multiprocessor Programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco (2008)"},{"issue":"10","key":"26_CR28","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"4","key":"26_CR29","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5(4), 596\u2013619 (1983)","journal-title":"ACM TOPLAS"},{"issue":"1","key":"26_CR30","first-page":"2:1","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Sys. 32(1), 2:1\u20132:70 (2014)","journal-title":"ACM Trans. Comput. Sys."},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S., Walker, D.: Linear maps. In: PLPV, pp. 3\u201314 (2011)","DOI":"10.1145\/1929529.1929531"},{"key":"26_CR32","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2004","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2004)"},{"key":"26_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-00590-9_27","volume-title":"Programming Languages and Systems","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378\u2013393. Springer, Heidelberg (2009)"},{"issue":"1","key":"26_CR34","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2576235","volume":"36","author":"H Liang","year":"2014","unstructured":"Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst. 36(1), 3:1\u20133:55 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"12","key":"26_CR35","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"issue":"1\u20133","key":"26_CR36","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"KL McMillan","year":"2000","unstructured":"McMillan, K.L.: A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1\u20133), 279\u2013309 (2000)","journal-title":"Sci. Comput. Program."},{"issue":"1\u20133","key":"26_CR37","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR38","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs i. Acta Inf. 6, 319\u2013340 (1976)","journal-title":"Acta Inf."},{"key":"26_CR39","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"26_CR40","doi-asserted-by":"crossref","unstructured":"Turon, A.J., Wand, M.: A separation logic for refining concurrent objects. In: Proceedings 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011), pp. 247\u2013258. ACM, New York (2011)","DOI":"10.1145\/1926385.1926415"},{"key":"26_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"26_CR42","unstructured":"Wadler, P.: Linear types can change the world!. In: Programming Concepts and Methods, North (1990)"},{"issue":"4","key":"26_CR43","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221\u2013227 (1971)","journal-title":"Commun. ACM"}],"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-319-21668-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:45:41Z","timestamp":1748493941000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}