{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:48Z","timestamp":1779087708867,"version":"3.51.4"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["101002697"],"award-info":[{"award-number":["101002697"]}]},{"name":"NSF","award":["CCF-2008083"],"award-info":[{"award-number":["CCF-2008083"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is a gap when programs also exploit nondeterminism(for concurrency, efficiency, or algorithmic design). In this paper, we introduce\n                    <jats:italic toggle=\"yes\">Demonic Outcome Logic<\/jats:italic>\n                    for reasoning about programs that exploit\n                    <jats:italic toggle=\"yes\">both<\/jats:italic>\n                    randomization and nondeterminism. The logic includes several novel features, such as reasoning about multiple executions in tandem and manipulating pre- and postconditions using familiar equational laws\u2014including the distributive law of probabilistic choices over nondeterministic ones. We also give rules for loops that both establish termination and quantify the distribution of final outcomes from a single premise. We illustrate the reasoning capabilities of Demonic Outcome Logic through several case studies, including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a heuristic based probabilistic SAT solver.\n                  <\/jats:p>","DOI":"10.1145\/3704855","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"539-568","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["A Demonic Outcome Logic for Randomized Nondeterminism"],"prefix":"10.1145","volume":"9","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":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8007-4725","authenticated-orcid":false,"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571195"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0083084"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:10)2021"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Filippo Bonchi Ana Sokolova and Valeria Vignudelli. 2019. The Theory of Traces for Systems with Nondeterminism and Probability. In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201314. https:\/\/doi.org\/10.1109\/lics.2019.8785673 10.1109\/lics.2019.8785673","DOI":"10.1109\/lics.2019.8785673"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CALCO.2021.11"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:21)2022"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_22"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656437"},{"key":"e_1_3_2_14_1","volume-title":"Comparative semantics for a process language with probabilistic choice and non-determinism","author":"den Hartog Jerry","year":"1998","unstructured":"Jerry den Hartog. 1998. Comparative semantics for a process language with probabilistic choice and non-determinism. Vrije Universiteit, Netherlands. Imported from DIES."},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46674-6_11"},{"key":"e_1_3_2_16_1","volume-title":"Probabilistic Extensions of Semantical Models","author":"den Hartog Jerry","year":"2002","unstructured":"Jerry den Hartog. 2002. Probabilistic Extensions of Semantical Models. Ph.D. Dissertation. Vrije Universiteit Amsterdam. https:\/\/core.ac.uk\/reader\/15452110"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82521-6"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_19_1","first-page":"1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall. I\u2013XVII, 1\u2013217 pages."},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571223"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3310131"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAP.2011.04.005"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.023"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470678"},{"key":"e_1_3_2_27_1","volume-title":"Probabilistic Non-determinism","author":"Jones Claire","year":"1990","unstructured":"Claire Jones. 1990. Probabilistic Non-determinism. Ph.D. Dissertation. University of Edinburgh. http:\/\/hdl.handle.net\/1842\/413"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Claire Jones and Gordon Plotkin. 1989. A Probabilistic Powerdomain of Evaluations. In Fourth Annual Symposium on Logic in Computer Science. 186\u2013195. https:\/\/doi.org\/10.1109\/lics.1989.39173 10.1109\/lics.1989.39173","DOI":"10.1109\/lics.1989.39173"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.18154\/RWTH-2019-01829"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:2)2017"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-61716-4_11"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288637"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00208-5"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.28"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_26"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.04.019"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf01213492"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_45_1","volume-title":"Monad Composition via Preservation of Algebras","author":"Parlant Louis","year":"2020","unstructured":"Louis Parlant. 2020. Monad Composition via Preservation of Algebras. Ph.D. Dissertation. University College London. https:\/\/discovery.ucl.ac.uk\/id\/eprint\/10112228\/"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Robert Rand and Steve Zdancewic. 2015. VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. In Electronic Notes in Theoretical Computer Science Vol. 319. 351\u2013367. https:\/\/doi.org\/10.1016\/j.entcs.2015.12.021 10.1016\/j.entcs.2015.12.021 The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI).","DOI":"10.1016\/j.entcs.2015.12.021"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0073967"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/239648"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015027"},{"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.1093\/comjnl\/35.5.514"},{"key":"e_1_3_2_53_1","volume-title":"Verifying Concurrent Randomized Algorithms","author":"Tassarotti Joseph","year":"2018","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","volume-title":"Continuous D-cones: convexity and powerdomain constructions","author":"Tix Regina","year":"1999","unstructured":"Regina Tix. 1999. Continuous D-cones: convexity and powerdomain constructions. Ph.D. Dissertation. Darmstadt University of Technology, Germany. https:\/\/d-nb.info\/957239157"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80746-7"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.01.002"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","unstructured":"Daniele Varacca. 2002. The powerdomain of indexed valuations. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. 299\u2013308. https:\/\/doi.org\/10.1109\/LICS.2002.1029838 10.1109\/LICS.2002.1029838","DOI":"10.1109\/LICS.2002.1029838"},{"key":"e_1_3_2_59_1","volume-title":"Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation","author":"Varacca Daniele","year":"2003","unstructured":"Daniele Varacca. 2003. Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation. Ph.D. Dissertation. University of Aarhus. https:\/\/www.brics.dk\/DS\/03\/14\/"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"},{"key":"e_1_3_2_61_1","first-page":"36","volume-title":"Monte Carlo Method","author":"von Neumann John","year":"1951","unstructured":"John von Neumann. 1951. Various techniques used in connection with random digits. In Monte Carlo Method, A.S. Householder, G.E. Forsythe, and H.H. Germond (Eds.). National Bureau of Standards Applied Mathematics Series, 12, Washington, D.C.: U.S. Government Printing Office, 36\u201338."},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689740"},{"key":"e_1_3_2_63_1","doi-asserted-by":"crossref","unstructured":"Noam Zilberstein. 2024. Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects. arXiv:2401.04594 [cs.LO]","DOI":"10.1145\/3743131"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"},{"key":"e_1_3_2_65_1","unstructured":"Noam Zilberstein Dexter Kozen Alexandra Silva and Joseph Tassarotti. 2024a. A Demonic Outcome Logic for Randomized Nondeterminism (Extended Version). arXiv:2410.22540 [cs.LO] https:\/\/arxiv.org\/abs\/2410.22540"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649821"},{"key":"e_1_3_2_67_1","volume-title":"On the Non-Compositionality of Monads via Distributive Laws","author":"Zwart Maaike","year":"2020","unstructured":"Maaike Zwart. 2020. On the Non-Compositionality of Monads via Distributive Laws. Ph.D. Dissertation. University of Oxford. https:\/\/ora.ox.ac.uk\/objects\/uuid:b2222b14-3895-4c87-91f4-13a8d046febb"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","unstructured":"Maaike Zwart and Dan Marsden. 2019. No-Go Theorems for Distributive Laws. In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201313. 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\/10.1145\/3704855","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704855","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:17Z","timestamp":1770200177000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704855"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":67,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704855"],"URL":"https:\/\/doi.org\/10.1145\/3704855","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}