POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Thu 23 Jan 2025 14:00 - 14:20 at Peek-A-Boo - Program Logics 1 Chair(s): Derek Dreyer

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 \emph{Demonic Outcome Logic} for reasoning about programs that exploit {\em both} 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—including 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.

Thu 23 Jan

Displayed time zone: Mountain Time (US & Canada) change

13:20 - 14:20
Program Logics 1POPL at Peek-A-Boo
Chair(s): Derek Dreyer MPI-SWS
13:20
20m
Talk
Program logics Ă  la carte
POPL
Max Vistrup ETH Zurich, Michael Sammler Institute of Science and Technology Austria, Ralf Jung ETH Zurich
13:40
20m
Talk
On Extending Incorrectness Logic with Backwards Reasoning
POPL
Freek Verbeek Open Universiteit & Virginia Tech, Md Syadus Sefat Virginia Tech, Zhoulai Fu State University of New York, Korea, Binoy Ravindran Virginia Tech
14:00
20m
Talk
A Demonic Outcome Logic for Randomized Nondeterminism
POPL
Noam Zilberstein Cornell University, Dexter Kozen Cornell University, Alexandra Silva Cornell University, Joseph Tassarotti New York University