{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:15:42Z","timestamp":1784211342672,"version":"3.55.0"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"NSF","award":["2504142,2504143"],"award-info":[{"award-number":["2504142,2504143"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    Although randomization has long been used in distributed computing, formal methods for reasoning aboutprobabilistic concurrent programs have lagged behind. No existing program logics can express specificationsabout the full\n                    <jats:italic toggle=\"yes\">distributions of outcomes<\/jats:italic>\n                    resulting from programs that are both probabilistic and concurrent. To address this, we introduce\n                    <jats:italic toggle=\"yes\">Probabilistic Concurrent Outcome Logic<\/jats:italic>\n                    (\n                    <jats:sc>pcOL<\/jats:sc>\n                    ), which incorporates ideas fromconcurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoningprinciples. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separationmodels probabilistic independence, so as to compositionally describe joint distributions over variables inconcurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to deriveprecise information about threads that rely on randomized shared state. We demonstrate\n                    <jats:sc>pcOL<\/jats:sc>\n                    on a variety ofexamples, including to prove almost sure termination of unbounded loops.\n                  <\/jats:p>","DOI":"10.1145\/3776651","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"235-264","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6388-063X","authenticated-orcid":false,"given":"Noam","family":"Zilberstein","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5692-3347","authenticated-orcid":false,"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_3_2_4_1","unstructured":"Axel Bacher Olivier Bodini Alexandros Hollender and J\u00e9r\u00e9mie Lumbroso. 2015. MergeShuffle: A Very Fast Parallel Random Permutation Algorithm. arXiv:1508.03167. https:\/\/arxiv.org\/abs\/1508.03167"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Jialu Bao Simon Docherty Justin Hsu and Alexandra Silva. 2021. A Bunched Logic for Conditional Independence. In Proceedings of the 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201921). Association for Computing Machinery New York NY USA 1 14. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470712 10.1109\/LICS52264.2021.9470712","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704894"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548719"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"Michael Ben-Or. 1983. Another Advantage of Free Choice (Extended Abstract): Completely Asynchronous Agreement Protocols. In Proceedings of the 2nd Annual ACM Symposium on Principles of Distributed Computing (PODC \u201983). Association for Computing Machinery New York NY USA 27 30. https:\/\/doi.org\/10.1145\/800221.806708 10.1145\/800221.806708","DOI":"10.1145\/800221.806708"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Lars Birkedal and Hongseok Yang. 2007. Relational Parametricity and Separation Logic. In Foundations of Software Science and Computation Structures. Springer Berlin Heidelberg 93 107. https:\/\/doi.org\/10.1007\/978-3-540-71389-0_8 10.1007\/978-3-540-71389-0_8","DOI":"10.1007\/978-3-540-71389-0_8"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","unstructured":"Stephen Brookes. 2004. A Semantics for Concurrent Separation Logic. In CONCUR 2004 \u2013 Concurrency Theory. Philippa Gardner and Nobuko Yoshida (Eds.).Springer Berlin Heidelberg 16 34. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_2 10.1007\/978-3-540-28644-8_2","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Peter W. O\u2019Hearn and Hongseok Yang. 2007. Local Action and Abstract Separation Logic. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007). 366 378. https:\/\/doi.org\/10.1109\/LICS.2007.30 10.1109\/LICS.2007.30","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/293347.293350"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","unstructured":"Leonardo de Moura Soonho Kong Jeremy Avigad Floris van Doorn and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction \u2013 CADE-25. Amy P. Felty and Aart Middeldorp (Eds.).Springer International Publishing Cham 378 388. https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26 10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_17_1","unstructured":"Simon Docherty. 2019. Bunched Logics: a Uniform Approach. Ph.D. Dissertation. University College London. https:\/\/discovery.ucl.ac.uk\/id\/eprint\/10073115\/"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Weijie Fan Florian Feng and Ilya Sergey. 2025. A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model. In Programming Languages and Systems. Viktor Vafeiadis (Ed.).Springer Nature Switzerland AG Cham 322 348. https:\/\/doi.org\/10.1007\/978-3-031-91118-7_13 10.1007\/978-3-031-91118-7_13","DOI":"10.1007\/978-3-031-91118-7_13"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Ira Dresfeld Joost-Pieter Katoen and Thomas Noll. 2022. Towards Concurrent Quantitative Separation Logic. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Bartek Klin Slawomir Lasota and Anna Muscholl (Eds.).Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 25:1 25:24. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.25 10.4230\/LIPIcs.CONCUR.2022.25","DOI":"10.4230\/LIPIcs.CONCUR.2022.25"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_3_2_21_1","unstructured":"Ronald A. Fisher and Frank Yates. 1938. Statistical Tables for Biological Agricultural and Medical Research(4th ed.).Oliver and Boyd Edinburgh."},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01934993"},{"key":"e_1_3_2_23_1","unstructured":"David Fremlin. 2001. Measure Theory Volume 2."},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90124-7"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674632"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_3_2_28_1","unstructured":"Philipp G. Haselwarter Kwing Hei Li Alejandro Aguirre Simon Oddershede Gregersen Joseph Tassarotti and Lars Birkedal. 2024. Approximate Relational Reasoning for Higher-Order Probabilistic Programs. arXiv:2407.14107. https:\/\/arxiv.org\/abs\/2407.14107"},{"key":"e_1_3_2_29_1","doi-asserted-by":"crossref","unstructured":"Philipp G. Haselwarter Kwing Hei Li Markus de Medeiros Simon Oddershede Gregersen Alejandro Aguirre Joseph Tassarotti and Lars Birkedal. 2024. Tactics: Higher-Order Separation Logic with Credits for Expected Costs. arXiv:2405.20083. https:\/\/arxiv.org\/abs\/2405.20083","DOI":"10.1145\/3689753"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.023"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung David Swasey Filip Siek Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915). Association for Computing Machinery New York NY USA 637 650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:2)2017"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"Daniil Lehmann and Michael O. Rabin. 1981. On the Advantages of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem. In Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201981). Association for Computing Machinery New York NY USA 133 138. https:\/\/doi.org\/10.1145\/567532.567547 10.1145\/567532.567547","DOI":"10.1145\/567532.567547"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591226"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3747514"},{"key":"e_1_3_2_39_1","unstructured":"Janine Lohse and Deepak Garg. 2024. An Iris for Expected Cost Analysis. arXiv:2406.00884. https:\/\/arxiv.org\/abs\/2406.00884"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"mathlib Community. 2020. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020). Association for Computing Machinery New York NY USA 367 381. https:\/\/doi.org\/10.1145\/3372885.3373824 10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"Carroll Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems. Springer. https:\/\/doi.org\/10.1007\/b138392 10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.01.016"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/359619.359627"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn. 2004. Resources Concurrency and Local Reasoning. In CONCUR 2004 \u2013 Concurrency Theory. Springer Berlin Heidelberg 49 67. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_3 10.1007\/978-3-540-28644-8_3","DOI":"10.1007\/978-3-540-28644-8_3"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn John C. Reynolds and Hongseok Yang. 2001. Local Reasoning about Programs That Alter Data Structures. In Computer Science Logic (CSL 2001). Springer Berlin Heidelberg 1 19. https:\/\/doi.org\/10.1007\/3-540-44802-0_1 10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01379149"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","unstructured":"Michael O. Rabin. 1980. N-Process Synchronization by 4 log2N-Valued Shared Variable. In 21st Annual Symposium on Foundations of Computer Science (FOCS 1980) 407 410. https:\/\/doi.org\/10.1109\/SFCS.1980.26 10.1109\/SFCS.1980.26","DOI":"10.1109\/SFCS.1980.26"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","unstructured":"John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002) 55 74. https:\/\/doi.org\/10.1109\/LICS.2002.1029817 10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_50_1","unstructured":"H. L. Royden. 1968. Real Analysis(2nd ed.).Macmillan New York."},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90048-X"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729284"},{"key":"e_1_3_2_53_1","unstructured":"Joseph Tassarotti. 2018. Verifying Concurrent Randomized Algorithms. Ph.D. Dissertation. Carnegie Mellon University. https:\/\/csd.cmu.edu\/academics\/doctoral\/degrees-conferred\/joseph-tassarotti"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.01.002"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","unstructured":"Daniele Varacca. 2002. The Powerdomain of Indexed Valuations. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002) 299 308. https:\/\/doi.org\/10.1109\/LICS.2002.1029838 10.1109\/LICS.2002.1029838","DOI":"10.1109\/LICS.2002.1029838"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","unstructured":"Simon Spies Anna Linn Georges Ahrens and Lars Birkedal. 2025. The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. In Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP \u201925). Association for Computing Machinery New York NY USA 83 97. https:\/\/doi.org\/10.1145\/3703595.3705876 10.1145\/3703595.3705876","DOI":"10.1145\/3703595.3705876"},{"key":"e_1_3_2_60_1","unstructured":"John von Neumann. 1951. Various Techniques Used in Connection with Random Digits. In Monte Carlo Method. G. E. Forsythe and H. H. Germond (Eds.).National Bureau of Standards Washington D.C. U.S. Government Printing Office 12 36 38."},{"key":"e_1_3_2_61_1","unstructured":"John von Neumann. 1951. Various Techniques Used in Connection with Random Digits. In Monte Carlo Method. G. E. Forsythe and H. H. Germond (Eds.).National Bureau of Standards Washington D.C. U.S. Government Printing Office 12 36 38."},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3743131"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586056"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704855"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649821"},{"key":"e_1_3_2_66_1","unstructured":"Noam Zilberstein and Alexandra Silva. 2025. Probabilistic Concurrent Reasoning in Outcome Logic: Independence Conditioning and Invariants (Full Version). arXiv:2411.11662. https:\/\/arxiv.org\/abs\/2411.11662"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","unstructured":"Maike Zwart and Dan Marsden. 2019. No-Go Theorems for Distributive Laws. In 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2019) 1 13. https:\/\/doi.org\/10.1109\/LICS.2019.8785707 10.1109\/LICS.2019.8785707","DOI":"10.1109\/LICS.2019.8785707"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776651","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776651","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:40:13Z","timestamp":1784209213000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776651"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":66,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776651"],"URL":"https:\/\/doi.org\/10.1145\/3776651","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-02","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}