{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:29:17Z","timestamp":1784255357855,"version":"3.55.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100007601","name":"Horizon 2020","doi-asserted-by":"publisher","award":["731453"],"award-info":[{"award-number":["731453"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003130","name":"Fonds Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003130","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007601","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["683289"],"award-info":[{"award-number":["683289"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>\n            Early in the development of Hoare logic, Owicki and Gries introduced\n            <jats:italic>auxiliary variables<\/jats:italic>\n            as a way of encoding information about the\n            <jats:italic>history<\/jats:italic>\n            of a program\u2019s execution that is useful for verifying its correctness. Over a decade later, Abadi and Lamport observed that it is sometimes also necessary to know in advance what a program will do in the\n            <jats:italic>future<\/jats:italic>\n            . To address this need, they proposed\n            <jats:italic>prophecy variables<\/jats:italic>\n            , originally as a proof technique for refinement mappings between state machines. However, despite the fact that prophecy variables are a clearly useful reasoning mechanism, there is (surprisingly) almost no work that attempts to integrate them into Hoare logic. In this paper, we present the first account of prophecy variables in a Hoare-style program logic that is flexible enough to verify\n            <jats:italic>logical atomicity<\/jats:italic>\n            (a relative of linearizability) for classic examples from the concurrency literature like RDCSS and the Herlihy-Wing queue. Our account is formalized in the Iris framework for separation logic in Coq. It makes essential use of\n            <jats:italic>ownership<\/jats:italic>\n            to encode the exclusive right to resolve a prophecy, which in turn enables us to enforce soundness of prophecies with a very simple set of proof rules.\n          <\/jats:p>","DOI":"10.1145\/3371113","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":51,"title":["The future is ours: prophecy variables in separation logic"],"prefix":"10.1145","volume":"4","author":[{"given":"Ralf","family":"Jung","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rodolphe","family":"Lepigre","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gaurav","family":"Parthasarathy","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland \/ MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marianna","family":"Rapoport","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada \/ MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_2_3_1","first-page":"55","article-title":"Checking interference with fractional permissions","volume":"2694","author":"Boyland John","year":"2003","unstructured":"John Boyland . 2003 . Checking interference with fractional permissions . In SAS (LNCS) , Vol. 2694. 55 \u2013 72 . John Boyland. 2003. Checking interference with fractional permissions. In SAS (LNCS), Vol. 2694. 55\u201372.","journal-title":"SAS (LNCS)"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926431"},{"key":"e_1_2_2_5_1","first-page":"207","article-title":"TaDA: A logic for time and data abstraction","volume":"8586","author":"da Rocha Pinto Pedro","year":"2014","unstructured":"Pedro da Rocha Pinto , Thomas Dinsdale-Young , and Philippa Gardner . 2014 . TaDA: A logic for time and data abstraction . In ECOOP (LNCS) , Vol. 8586. 207 \u2013 231 . Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A logic for time and data abstraction. In ECOOP (LNCS), Vol. 8586. 207\u2013231.","journal-title":"ECOOP (LNCS)"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371101"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.8"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. ReLoC: A mechanised relational logic for fine-grained concurrency. In LICS. 442\u2013451.  Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. ReLoC: A mechanised relational logic for fine-grained concurrency. In LICS. 442\u2013451.","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_10_1","first-page":"388","article-title":"Reasoning about optimistic concurrency using a program logic for history","volume":"6269","author":"Fu Ming","year":"2010","unstructured":"Ming Fu , Yong Li , Xinyu Feng , Zhong Shao , and Yu Zhang . 2010 . Reasoning about optimistic concurrency using a program logic for history . In CONCUR (LNCS) , Vol. 6269. 388 \u2013 402 . Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. 2010. Reasoning about optimistic concurrency using a program logic for history. In CONCUR (LNCS), Vol. 6269. 388\u2013402.","journal-title":"CONCUR (LNCS)"},{"key":"e_1_2_2_11_1","volume-title":"Pratt","author":"Harris Timothy L.","year":"2002","unstructured":"Timothy L. Harris , Keir Fraser , and Ian A . Pratt . 2002 . A practical multi-word compare-and-swap operation. In DISC. Timothy L. Harris, Keir Fraser, and Ian A. Pratt. 2002. A practical multi-word compare-and-swap operation. In DISC."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Bart Jacobs and Frank Piessens. 2011. Expressive modular fine-grained concurrency specification. In POPL. 271\u2013282.  Bart Jacobs and Frank Piessens. 2011. Expressive modular fine-grained concurrency specification. In POPL. 271\u2013282.","DOI":"10.1145\/1925844.1926417"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Bart Jacobs Jan Smans Pieter Philippaerts Fr\u00e9d\u00e9ric Vogels Willem Penninckx and Frank Piessens. 2011. VeriFast: A powerful sound predictable fast verifier for C and Java. In NASA Formal Methods.  Bart Jacobs Jan Smans Pieter Philippaerts Fr\u00e9d\u00e9ric Vogels Willem Penninckx and Frank Piessens. 2011. VeriFast: A powerful sound predictable fast verifier for C and Java. In NASA Formal Methods.","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3570660"},{"key":"e_1_2_2_17_1","volume-title":"Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL. 637\u2013650.","author":"Jung Ralf","year":"2015","unstructured":"Ralf Jung , David Swasey , Filip Sieczkowski , Kasper Svendsen , Aaron Turon , Lars Birkedal , and Derek Dreyer . 2015 . Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL. 637\u2013650. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL. 637\u2013650."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217.  Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217.","DOI":"10.1145\/3093333.3009855"},{"key":"e_1_2_2_20_1","volume-title":"Auxiliary variables in TLA+. CoRR abs\/1703.05121","author":"Lamport Leslie","year":"2017","unstructured":"Leslie Lamport and Stephan Merz . 2017. Auxiliary variables in TLA+. CoRR abs\/1703.05121 ( 2017 ). http:\/\/arxiv.org\/abs\/ 1703.05121 Leslie Lamport and Stephan Merz. 2017. Auxiliary variables in TLA+. CoRR abs\/1703.05121 (2017). http:\/\/arxiv.org\/abs\/ 1703.05121"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective auxiliary state for coarse-grained concurrency. In POPL. 561\u2013574.  Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective auxiliary state for coarse-grained concurrency. In POPL. 561\u2013574.","DOI":"10.1145\/2480359.2429134"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In PLDI.  Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In PLDI.","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3340672.3341118"},{"key":"e_1_2_2_27_1","unstructured":"John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. 55\u201374.  John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. 55\u201374."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_2_29_1","volume-title":"Tressa: Claiming the future. In VST TE.","author":"Sezgin Ali","year":"2010","unstructured":"Ali Sezgin , Serdar Tasiran , and Shaz Qadeer . 2010 . Tressa: Claiming the future. In VST TE. Ali Sezgin, Serdar Tasiran, and Shaz Qadeer. 2010. Tressa: Claiming the future. In VST TE."},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Aaron Turon Jacob Thamsborg Amal Ahmed Lars Birkedal and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In POPL.  Aaron Turon Jacob Thamsborg Amal Ahmed Lars Birkedal and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In POPL.","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_2_33_1","first-page":"256","article-title":"A marriage of rely\/guarantee and separation logic","volume":"4703","author":"Vafeiadis Viktor","year":"2007","unstructured":"Viktor Vafeiadis and Matthew J. Parkinson . 2007 . A marriage of rely\/guarantee and separation logic . In CONCUR (LNCS) , Vol. 4703. 256 \u2013 271 . Viktor Vafeiadis and Matthew J. Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In CONCUR (LNCS), Vol. 4703. 256\u2013271.","journal-title":"CONCUR (LNCS)"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29952-0_12"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371113","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371113","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371113"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371113"],"URL":"https:\/\/doi.org\/10.1145\/3371113","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}