{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:25:49Z","timestamp":1750843549546,"version":"3.40.3"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030393212"},{"type":"electronic","value":"9783030393229"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[[2020]]},"DOI":"10.1007\/978-3-030-39322-9_19","type":"book-chapter","created":{"date-parts":[[2020,1,14]],"date-time":"2020-01-14T19:03:59Z","timestamp":1579028639000},"page":"401-425","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Practical Abstractions for Automated Verification of Shared-Memory Concurrency"],"prefix":"10.1007","author":[{"given":"Wytse","family":"Oortwijn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,1,13]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84800-223-4","volume-title":"A Process Algebraic Approach to Software Architecture Design","author":"A Aldini","year":"2010","unstructured":"Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, London (2010). https:\/\/doi.org\/10.1007\/978-1-84800-223-4"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5\u201321. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74591-4_3"},{"key":"19_CR3","doi-asserted-by":"publisher","unstructured":"Appel, A., Melli\u00e8s, P., Richards, C., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL, vol. 42, pp. 109\u2013122. ACM (2007). https:\/\/doi.org\/10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"19_CR4","unstructured":"Baeten, J.: Process Algebra with Explicit Termination. Eindhoven University of Technology, Department of Mathematics and Computing Science (2000)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-662-46675-9_14","volume-title":"Fundamental Approaches to Software Engineering","author":"S Blom","year":"2015","unstructured":"Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 202\u2013217. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_14"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-319-22969-0_6","volume-title":"Software Engineering and Formal Methods","author":"S Blom","year":"2015","unstructured":"Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-based verification of functional behaviour of concurrent programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84\u201398. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_6"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55\u201372. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"issue":"1\u20133","key":"19_CR9","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1\u20133), 227\u2013270 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.034","journal-title":"Theor. Comput. Sci."},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-74061-2_15","volume-title":"Static Analysis","author":"C Calcagno","year":"2007","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233\u2013248. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_15"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504\u2013528. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24"},{"key":"19_CR12","doi-asserted-by":"publisher","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL, vol. 44, pp. 315\u2013327. ACM (2009). https:\/\/doi.org\/10.1145\/1480881.1480922","DOI":"10.1145\/1480881.1480922"},{"key":"19_CR13","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). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_13"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-22110-1_32","volume-title":"Computer Aided Verification","author":"A Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Threader: a constraint-based verifier for multi-threaded programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 412\u2013417. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_32"},{"issue":"3","key":"19_CR15","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.: Linearizability: a correctness condition for concurrent objects. TOPLAS 12(3), 463\u2013492 (1990). https:\/\/doi.org\/10.1145\/78969.78972","journal-title":"TOPLAS"},{"key":"19_CR16","unstructured":"Hobor, A.: Oracle semantics. Ph.D. thesis, Princeton University (2008)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-78739-6_27","volume-title":"Programming Languages and Systems","author":"A Hobor","year":"2008","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 353\u2013367. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78739-6_27"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0053567","volume-title":"Programming Languages and Systems","author":"K Honda","year":"1998","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122\u2013138. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0053567"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"issue":"4","key":"19_CR20","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C Jones","year":"1983","unstructured":"Jones, C.: Tentative steps toward a development method for interfering programs. TOPLAS 5(4), 596\u2013619 (1983). https:\/\/doi.org\/10.1145\/69575.69577","journal-title":"TOPLAS"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Joosten, S., Oortwijn, W., Safari, M., Huisman, M.: An exercise in verifying sequential programs with VerCors. In: Summers, A. (ed.) FTfJP, pp. 40\u201345. ACM (2018). https:\/\/doi.org\/10.1145\/3236454.3236479","DOI":"10.1145\/3236454.3236479"},{"key":"19_CR22","unstructured":"Juhasz, U., Kassios, I., M\u00fcller, P., Novacek, M., Schwerhoff, M., Summers, A.: Viper: a verification infrastructure for permission-based reasoning. Technical report, ETH Z\u00fcrich (2014)"},{"key":"19_CR23","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: ICFP, vol. 51, pp. 256\u2013269. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"19_CR24","doi-asserted-by":"publisher","unstructured":"Jung, R., et al.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, vol. 50, pp. 637\u2013650. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-662-54434-1_26","volume-title":"Programming Languages and Systems","author":"R Krebbers","year":"2017","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696\u2013723. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26"},{"key":"19_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158125","volume":"2","author":"S Krishna","year":"2017","unstructured":"Krishna, S., Shasha, D., Wies, T.: Go with the flow: compositional abstractions for concurrent data structures. POPL 2, 1\u201331 (2017). https:\/\/doi.org\/10.1145\/3158125","journal-title":"POPL"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03829-7_7","volume-title":"Foundations of Security Analysis and Design V","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 195\u2013222. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_7"},{"key":"19_CR28","doi-asserted-by":"publisher","unstructured":"Luo, Z., Zheng, M., Siegel, S.: Verification of MPI programs using CIVL. In: EuroMPI. ACM (2017). https:\/\/doi.org\/10.1145\/3127024.3127032","DOI":"10.1145\/3127024.3127032"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-54833-8_16","volume-title":"Programming Languages and Systems","author":"A Nanevski","year":"2014","unstructured":"Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 290\u2013310. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_16"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-02146-7_11","volume-title":"Formal Aspects of Component Software","author":"T Neele","year":"2018","unstructured":"Neele, T., Willemse, T.A.C., Groote, J.F.: Solving parameterised Boolean equation systems with infinite data through quotienting. In: Bae, K., \u00d6lveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 216\u2013236. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02146-7_11"},{"issue":"1\u20133","key":"19_CR32","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.035","journal-title":"Theor. Comput. Sci."},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: POPL, vol. 39, pp. 268\u2013280. ACM (2004). https:\/\/doi.org\/10.1145\/964001.964024","DOI":"10.1145\/964001.964024"},{"key":"19_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-319-72308-2_12","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"W Oortwijn","year":"2017","unstructured":"Oortwijn, W., Blom, S., Gurov, D., Huisman, M., Zaharieva-Stojanovski, M.: An abstraction technique for describing concurrent program behaviour. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 191\u2013209. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72308-2_12"},{"key":"19_CR35","doi-asserted-by":"publisher","first-page":"65","DOI":"10.4204\/EPTCS.211.7","volume":"211","author":"Wytse Oortwijn","year":"2016","unstructured":"Oortwijn, W., Blom, S., Huisman, M.: Future-based static analysis of message passing programs. In: Programming Language Approaches to Concurrency- & Communication-cEntric Software (PLACES), pp. 65\u201372. Open Publishing Association (2016). https:\/\/doi.org\/10.4204\/EPTCS.211.7","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"19_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-030-34968-4_23","volume-title":"Integrated Formal Methods","author":"W Oortwijn","year":"2019","unstructured":"Oortwijn, W., Huisman, M.: Formal verification of an industrial safety-critical traffic tunnel control system. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) IFM 2019. LNCS, vol. 11918, pp. 418\u2013436. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_23"},{"key":"19_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-030-34968-4_22","volume-title":"Integrated Formal Methods","author":"W Oortwijn","year":"2019","unstructured":"Oortwijn, W., Huisman, M.: Practical abstractions for automated verification of message passing concurrency. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) IFM 2019. LNCS, vol. 11918, pp. 399\u2013417. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_22"},{"key":"19_CR38","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1975","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6, 319\u2013340 (1975)","journal-title":"Acta Informatica"},{"key":"19_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-19718-5_23","volume-title":"Programming Languages and Systems","author":"MJ Parkinson","year":"2011","unstructured":"Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 439\u2013458. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_23"},{"key":"19_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-662-46669-8_7","volume-title":"Programming Languages and Systems","author":"W Penninckx","year":"2015","unstructured":"Penninckx, W., Jacobs, B., Piessens, F.: Sound, modular and compositional verification of the input\/output behavior of programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 158\u2013182. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_7"},{"key":"19_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P da Rocha Pinto","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9"},{"key":"19_CR42","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2015.12.002","volume":"319","author":"Pedro da Rocha Pinto","year":"2015","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: Steps in modular specifications for concurrent modules. In: MFPS, pp. 3\u201318 (2015). https:\/\/doi.org\/10.1016\/j.entcs.2015.12.002","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"19_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-662-46669-8_14","volume-title":"Programming Languages and Systems","author":"I Sergey","year":"2015","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Specifying and verifying concurrent algorithms with histories and subjectivity. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 333\u2013358. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_14"},{"key":"19_CR44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158116","volume":"2","author":"I Sergey","year":"2017","unstructured":"Sergey, I., Wilcox, J., Tatlock, Z.: Programming and proving with distributed protocols. POPL 2, 1\u201330 (2017). https:\/\/doi.org\/10.1145\/3158116","journal-title":"POPL"},{"key":"19_CR45","doi-asserted-by":"publisher","unstructured":"Siegel, S., et al.: CIVL: the concurrency intermediate verification language. In: International Conference for High Performance Computing, Networking, Storage and Analysis (SC), p. 61. ACM (2015). https:\/\/doi.org\/10.1145\/2807591.2807635","DOI":"10.1145\/2807591.2807635"},{"key":"19_CR46","unstructured":"Supplementary Material. The supplementary material for this paper, consisting of a technical report, the Coq formalisation and the case study, can be found online at https:\/\/github.com\/wytseoortwijn\/VMCAI20-SharedMemAbstr"},{"key":"19_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1007\/978-3-662-49498-1_27","volume-title":"Programming Languages and Systems","author":"AJ Summers","year":"2016","unstructured":"Summers, A.J., M\u00fcller, P.: Actor services \u2013 modular verification of message passing programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 699\u2013726. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_27"},{"key":"19_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9"},{"key":"19_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-37036-6_11","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2013","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Modular reasoning about separation of concurrent data structures. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 169\u2013188. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_11"},{"key":"19_CR50","doi-asserted-by":"publisher","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377\u2013390. ACM (2013). https:\/\/doi.org\/10.1145\/2500365.2500600","DOI":"10.1145\/2500365.2500600"},{"key":"19_CR51","unstructured":"Usenko, Y.: Linearization in $$\\mu CRL$$. Technische Universiteit Eindhoven (2002)"},{"key":"19_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450\u2013464. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_40"},{"key":"19_CR53","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/j.entcs.2011.09.029","volume":"276","author":"Viktor Vafeiadis","year":"2011","unstructured":"Vafeiadis, V.: Concurrent separation logic and operational semantics. In: MFPS, volume 276 of ENTCS, pp. 335\u2013351 (2011). https:\/\/doi.org\/10.1016\/j.entcs.2011.09.029","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"19_CR54","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). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18"},{"key":"19_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-10672-9_15","volume-title":"Programming Languages and Systems","author":"J Villard","year":"2009","unstructured":"Villard, J., Lozes, \u00c9., Calcagno, C.: Proving copyless message passing. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 194\u2013209. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_15"},{"key":"19_CR56","doi-asserted-by":"publisher","unstructured":"Zaharieva-Stojanovski, M.: Closer to reliable software: verifying functional behaviour of concurrent programs. Ph.D. thesis, University of Twente (2015). https:\/\/doi.org\/10.3990\/1.9789036539241","DOI":"10.3990\/1.9789036539241"},{"key":"19_CR57","doi-asserted-by":"publisher","unstructured":"Zheng, M., Rogers, M., Luo, Z., Dwyer, M., Siegel, S.: CIVL: formal verification of parallel programs. In: ASE, pp. 830\u2013835. IEEE (2015). https:\/\/doi.org\/10.1109\/ASE.2015.99","DOI":"10.1109\/ASE.2015.99"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-39322-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T18:43:30Z","timestamp":1710269010000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-39322-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030393212","9783030393229"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-39322-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 January 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Orleans, LA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2020a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl20.sigplan.org\/home\/VMCAI-2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}