Noam Zilberstein (Cornell)- Formal Foundations for Programs with Interacting Effects

Abstract: Critical software components often display effects such as randomization, nondeterminism, concurrency, and exceptions. Complex combinations of effects show up in distributed systems, security, and privacy applications where correctness is crucial, but mixtures of effects also make testing and informal reasoning difficult or impossible. While powerful formal methods exist for verifying programs with individual effects, those approaches do not provide a unified account of how such effects interact. As a result, verification techniques are highly specialized and difficult to compose.

In this talk, I present Outcome Logic, a logical foundation that captures diverse program behaviors via a common notion of outcomes. Outcome Logic enables reusable reasoning principles across deterministic, nondeterministic, and probabilistic settings, and allows multiple effects to be composed on top of the base logic. I will show how the extensible approach allows Outcome Logic to support new types of reasoning in domains such as verification of randomized distributed systems and principled bug-finding techniques.