{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:58Z","timestamp":1780994698480,"version":"3.54.1"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.<\/jats:p>","DOI":"10.1145\/3290377","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["A separation logic for concurrent randomized programs"],"prefix":"10.1145","volume":"3","author":[{"given":"Joseph","family":"Tassarotti","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Alejandro Aguirre Gilles Barthe Lars Birkedal Ales Bizjak Marco Gaboardi and Deepak Garg. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In ESOP. 214\u2013241.  Alejandro Aguirre Gilles Barthe Lars Birkedal Ales Bizjak Marco Gaboardi and Deepak Garg. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In ESOP. 214\u2013241.","DOI":"10.1007\/978-3-319-89884-1_8"},{"key":"e_1_2_2_2_1","volume-title":"Program Logics - for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel . 2014. Program Logics - for Certified Compilers . Cambridge University Press . Andrew W. Appel. 2014. Program Logics - for Certified Compilers. Cambridge University Press."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_2_2_5_1","unstructured":"Gilles Barthe Thomas Espitau Benjamin Gr\u00e9goire Justin Hsu and Pierre-Yves Strub. 2017a. Proving uniformity and independence by self-composition and coupling. In LPAR.  Gilles Barthe Thomas Espitau Benjamin Gr\u00e9goire Justin Hsu and Pierre-Yves Strub. 2017a. Proving uniformity and independence by self-composition and coupling. In LPAR."},{"key":"e_1_2_2_6_1","volume-title":"44th International Colloquium on Automata, Languages, and Programming, ICALP 2017","author":"Barthe Gilles","year":"2017","unstructured":"Gilles Barthe , Thomas Espitau , Justin Hsu , Tetsuya Sato , and Pierre-Yves Strub . 2017 b. *-Liftings for Differential Privacy. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017 , July 10-14, 2017, Warsaw, Poland. 102:1\u2013102:12. Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. 2017b. *-Liftings for Differential Privacy. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland. 102:1\u2013102:12."},{"key":"e_1_2_2_7_1","first-page":"1","article-title":"A Program Logic for Union Bounds","volume":"107","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe , Marco Gaboardi , Benjamin Gr\u00e9goire , Justin Hsu , and Pierre-Yves Strub . 2016 . A Program Logic for Union Bounds . In ICALP. 107 : 1 \u2013 107 :15. Gilles Barthe, Marco Gaboardi, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2016. A Program Logic for Union Bounds. In ICALP. 107:1\u2013107:15.","journal-title":"ICALP."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_1"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009896"},{"key":"e_1_2_2_10_1","volume-title":"Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll.","author":"Batz Kevin","year":"2018","unstructured":"Kevin Batz , Benjamin Lucien Kaminski , Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2018 . Quantitative Separation Logic. CoRR abs\/1802.10467 (2018). arXiv: 1802.10467 http:\/\/arxiv.org\/abs\/1802.10467 Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2018. Quantitative Separation Logic. CoRR abs\/1802.10467 (2018). arXiv: 1802.10467 http:\/\/arxiv.org\/abs\/1802.10467"},{"key":"e_1_2_2_11_1","volume-title":"Seminar on Triples and Categorical Homology Theory","author":"Beck Jon","unstructured":"Jon Beck . 1969. Distributive laws . In Seminar on Triples and Categorical Homology Theory , B. Eckmann (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 119\u2013140. Jon Beck. 1969. Distributive laws. In Seminar on Triples and Categorical Homology Theory, B. Eckmann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 119\u2013140."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_2_2_14_1","volume-title":"9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings. 1\u201316","author":"Boyd-Wickizer Silas","year":"2010","unstructured":"Silas Boyd-Wickizer , Austin T. Clements , Yandong Mao , Aleksey Pesterev , M. Frans Kaashoek , Robert Tappan Morris , and Nickolai Zeldovich . 2010 . An Analysis of Linux Scalability to Many Cores . In 9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings. 1\u201316 . Silas Boyd-Wickizer, Austin T. Clements, Yandong Mao, Aleksey Pesterev, M. Frans Kaashoek, Robert Tappan Morris, and Nickolai Zeldovich. 2010. An Analysis of Linux Scalability to Many Cores. In 9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings. 1\u201316."},{"key":"e_1_2_2_15_1","volume-title":"10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings. 55\u201372","author":"Boyland John","year":"2003","unstructured":"John Boyland . 2003 . Checking Interference with Fractional Permissions. In Static Analysis , 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings. 55\u201372 . John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings. 55\u201372."},{"key":"e_1_2_2_16_1","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","unstructured":"Adam Chlipala . 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant . MIT Press . http:\/\/mitpress.mit.edu\/books\/certified- programming- dependent- types Adam Chlipala. 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. http:\/\/mitpress.mit.edu\/books\/certified- programming- dependent- types"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486159.2486182"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"T. Dinsdale-Young M. Dodds P. Gardner M. Parkinson and V. Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP. 504\u2013528.   T. Dinsdale-Young M. Dodds P. Gardner M. Parkinson and V. Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP. 504\u2013528.","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Xinyu Feng Rodrigo Ferreira and Zhong Shao. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP. 173\u2013188.   Xinyu Feng Rodrigo Ferreira and Zhong Shao. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP. 173\u2013188.","DOI":"10.1007\/978-3-540-71316-6_13"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01934993"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","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. 388\u2013402.   Ming Fu Yong Li Xinyu Feng Zhong Shao and Yu Zhang. 2010. Reasoning about optimistic concurrency using a program logic for history. In CONCUR. 388\u2013402.","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993636.1993687"},{"key":"e_1_2_2_30_1","volume-title":"21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. 542\u2013557","author":"Goubault-Larrecq Jean","year":"2007","unstructured":"Jean Goubault-Larrecq . 2007 . Continuous Previsions. In Computer Science Logic , 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. 542\u2013557 . Jean Goubault-Larrecq. 2007. Continuous Previsions. In Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. 542\u2013557."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.09.003"},{"key":"e_1_2_2_32_1","unstructured":"Maurice Herlihy Yossi Lev Victor Luchangco and Nir Shavit. 2006. A Provably Correct Scalable Concurrent Skip List (Brief Announcement). In OPODIS.  Maurice Herlihy Yossi Lev Victor Luchangco and Nir Shavit. 2006. A Provably Correct Scalable Concurrent Skip List (Brief Announcement). In OPODIS."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_34_1","volume-title":"Probabilistic Couplings for Probabilistic Reasoning. ArXiv e-prints (Oct","author":"Hsu J.","year":"2017","unstructured":"J. Hsu . 2017. Probabilistic Couplings for Probabilistic Reasoning. ArXiv e-prints (Oct . 2017 ). arXiv: cs.LO\/1710.09951 J. Hsu. 2017. Probabilistic Couplings for Probabilistic Reasoning. ArXiv e-prints (Oct. 2017). arXiv: cs.LO\/1710.09951"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009877"},{"key":"e_1_2_2_43_1","volume-title":"Lectures on the Coupling Method","author":"Lindvall T.","unstructured":"T. Lindvall . 2002. Lectures on the Coupling Method . Dover Publications, Inc orporated. T. Lindvall. 2002. Lectures on the Coupling Method. Dover Publications, Incorporated."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.01.016"},{"key":"e_1_2_2_45_1","volume-title":"Nondeterminism and Probabilistic Choice: Obeying the Laws. In CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings. 350\u2013364","author":"Mislove Michael W.","year":"2000","unstructured":"Michael W. Mislove . 2000 . Nondeterminism and Probabilistic Choice: Obeying the Laws. In CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings. 350\u2013364 . Michael W. Mislove. 2000. Nondeterminism and Probabilistic Choice: Obeying the Laws. In CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings. 350\u2013364."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.113"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/359619.359627"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/78973.78977"},{"key":"e_1_2_2_55_1","unstructured":"John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS.   John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS."},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983999"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_30"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_59_1","unstructured":"Iris Team. 2017. Iris 3.0 Documentation. http:\/\/plv.mpi- sws.org\/iris\/appendix- 3.0.pdf  Iris Team. 2017. Iris 3.0 Documentation. http:\/\/plv.mpi- sws.org\/iris\/appendix- 3.0.pdf"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.01.002"},{"key":"e_1_2_2_61_1","volume-title":"Proceedings of the 32nd International Conference on Machine Learning, ICML 2015","author":"Tristan Jean-Baptiste","year":"2015","unstructured":"Jean-Baptiste Tristan , Joseph Tassarotti , and Guy L . Steele Jr. 2015. Efficient Training of LDA on a GP U by Mean-for-Mode Estimation . In Proceedings of the 32nd International Conference on Machine Learning, ICML 2015 , Lille, France , 6-11 July 2015 . 59\u201368. Jean-Baptiste Tristan, Joseph Tassarotti, and Guy L. Steele Jr. 2015. Efficient Training of LDA on a GP U by Mean-for-Mode Estimation. In Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015. 59\u201368."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_64_1","doi-asserted-by":"crossref","unstructured":"V. Vafeiadis and M. Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In CONCUR. 256\u2013271.   V. Vafeiadis and M. Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In CONCUR. 256\u2013271.","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"e_1_2_2_65_1","doi-asserted-by":"crossref","unstructured":"Eelis van der Weegen and James McKinna. 2008. A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. In TYPES. 256\u2013271.  Eelis van der Weegen and James McKinna. 2008. A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. In TYPES. 256\u2013271.","DOI":"10.1007\/978-3-642-02444-3_16"},{"key":"e_1_2_2_66_1","volume-title":"The Powerdomain of Indexed Valuations. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. 299","author":"Varacca Daniele","year":"2002","unstructured":"Daniele Varacca . 2002 . The Powerdomain of Indexed Valuations. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. 299 . Daniele Varacca. 2002. The Powerdomain of Indexed Valuations. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. 299."},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290377","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290377"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":63,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290377"],"URL":"https:\/\/doi.org\/10.1145\/3290377","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}