A Demonic Outcome Logic for Randomized Nondeterminism

This conference talk from POPL 2025 introduces Demonic Outcome Logic, a novel approach for reasoning about programs that combine both randomization and nondeterminism. Explore how researchers from Cornell University and New York University address a significant gap in program analysis for applications in cryptography and machine learning. The presentation covers innovative features of the logic, including reasoning about multiple executions simultaneously and manipulating pre- and postconditions using equational laws. Learn about rules for loops that establish termination and quantify distribution of final outcomes, with practical applications demonstrated through case studies including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a probabilistic SAT solver. The 18-minute video provides valuable insights for those interested in program logics and probabilistic programming with demonic nondeterminism.