{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:04Z","timestamp":1774025824767,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_13","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"357-384","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["A Separation Logic for a Promising Semantics"],"prefix":"10.1007","author":[{"given":"Kasper","family":"Svendsen","sequence":"first","affiliation":[]},{"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[]},{"given":"Marko","family":"Doko","sequence":"additional","affiliation":[]},{"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"13_CR1","unstructured":"Supplementary material for this paper. \nhttp:\/\/plv.mpi-sws.org\/slr\/appendix.pdf"},{"issue":"1","key":"13_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/3093333.3009883","volume":"52","author":"Jade Alglave","year":"2017","unstructured":"Alglave, J., Cousot, P.: Ogre and Pythia: an invariance proof method for weak consistency models. In: POPL 2017, pp. 3\u201318. ACM, New York (2017). \nhttp:\/\/doi.acm.org\/10.1145\/2994593","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-662-46669-8_12","volume-title":"Programming Languages and Systems","author":"M Batty","year":"2015","unstructured":"Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 283\u2013307. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46669-8_12"},{"issue":"1","key":"13_CR4","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/1925844.1926394","volume":"46","author":"Mark Batty","year":"2011","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL 2011, pp. 55\u201366. ACM, New York (2011). \nhttp:\/\/doi.acm.org\/10.1145\/1926385.1926394","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR5","unstructured":"Boehm, H.J., Demsky, B.: Outlawing ghosts: avoiding out-of-thin-air results. In: Proceedings of the Workshop on Memory Systems Performance and Correctness, MSPC 2014, pp. 7:1\u20137:6. ACM, New York (2014). \nhttp:\/\/doi.acm.org\/10.1145\/2618128.2618134"},{"key":"13_CR6","unstructured":"Bornat, R., Alglave, J., Parkinson, M.: New lace and arsenic (2016). \nhttps:\/\/arxiv.org\/abs\/1512.01416"},{"key":"13_CR7","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Robustness against relaxed memory models. In: Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik, 25\u201328 Februar 2014, Kiel, Deutschland, pp. 85\u201386 (2014)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-662-49122-5_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Doko","year":"2016","unstructured":"Doko, M., Vafeiadis, V.: A program logic for C11 memory fences. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 413\u2013430. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49122-5_20"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/978-3-662-54434-1_17","volume-title":"Programming Languages and Systems","author":"M Doko","year":"2017","unstructured":"Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 448\u2013475. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54434-1_17"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Jeffrey, A., Riely, J.: On thin air reads towards an event structures model of relaxed memory. In: LICS 2016, pp. 759\u2013767. ACM, New York (2016)","DOI":"10.1145\/2933575.2934536"},{"key":"13_CR11","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up (2017)"},{"key":"13_CR12","unstructured":"Kaiser, J.O., Dang, H.H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: reasoning about release-acquire consistency in Iris. In: ECOOP 2017 (2017)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: POPL 2017. ACM, New York (2017). \nhttp:\/\/doi.acm.org\/10.1145\/3009837.3009850","DOI":"10.1145\/3009837.3009850"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: PLDI (2017)","DOI":"10.1145\/3062341.3062352"},{"issue":"1","key":"13_CR15","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1145\/2914770.2837643","volume":"51","author":"Ori Lahav","year":"2016","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: POPL 2016, pp. 649\u2013662. ACM, New York (2016). \nhttp:\/\/doi.acm.org\/10.1145\/2837614.2837643","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-47666-6_25","volume-title":"Automata, Languages, and Programming","author":"O Lahav","year":"2015","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311\u2013323. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-47666-6_25"},{"issue":"1","key":"13_CR17","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1145\/1047659.1040336","volume":"40","author":"Jeremy Manson","year":"2005","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL, pp. 378\u2013391. ACM, New York (2005)","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14107-2_23","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"S Owens","year":"2010","unstructured":"Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 478\u2013503. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14107-2_23"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391\u2013407. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_27"},{"issue":"1","key":"13_CR20","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/2914770.2837616","volume":"51","author":"Jean Pichon-Pharabod","year":"2016","unstructured":"Pichon-Pharabod, J., Sewell, P.: A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In: POPL 2016, pp. 622\u2013633. ACM, New York (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR21","unstructured":"Podkopaev, A., Lahav, O., Vafeiadis, V.: Promising compilation to ARMv8 POP. In: ECOOP 2017. LIPIcs, vol. 74, pp. 22:1\u201322:28. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22\u201325 July 2002, Copenhagen, Denmark, pp. 55\u201374 (2002). \nhttps:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-15057-9_4","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T Ridge","year":"2010","unstructured":"Ridge, T.: A rely-guarantee proof system for x86-TSO. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 55\u201370. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-15057-9_4"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"736","DOI":"10.1007\/978-3-662-46669-8_30","volume-title":"Programming Languages and Systems","author":"F Sieczkowski","year":"2015","unstructured":"Sieczkowski, F., Svendsen, K., Birkedal, L., Pichon-Pharabod, J.: A separation logic for fictional sequential consistency. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 736\u2013761. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46669-8_30"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/978-3-662-49498-1_28","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2016","unstructured":"Svendsen, K., Sieczkowski, F., Birkedal, L.: Transfinite step-indexing: decoupling concrete and logical steps. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 727\u2013751. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49498-1_28"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Turon, A., Vafeiadis, V., Dreyer, D.: GPS: navigating weak memory with ghosts, protocols, and separation. In: 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2014, pp. 691\u2013707. ACM, New York (2014)","DOI":"10.1145\/2660193.2660243"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: OOPSLA 2013, pp. 867\u2013884. ACM, New York (2013)","DOI":"10.1145\/2509136.2509532"},{"key":"13_CR28","unstructured":"Wehrman, I., Berdine, J.: A proposal for weak-memory local reasoning. In: LOLA (2011)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89884-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:10:00Z","timestamp":1523653800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}