Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching

This video presents a research talk on "Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching" delivered by researchers James Li, Noam Zilberstein, and Alexandra Silva from Cornell University at the Theory and Practice of Static Analysis (TPSA) workshop in January 2025. Explore a novel unified logic framework that addresses the full spectrum of termination conditions in program analysis, eliminating the need for specialized logics for different termination guarantees. Learn how Total Outcome Logic extends beyond traditional approaches by incorporating reasoning about partial correctness, total correctness, and explicit nontermination proofs within a single system. Discover how this approach effectively handles various branching effects, including nondeterminism and randomization, providing a unified metatheory for termination reasoning across different types of programs. The 20-minute presentation is part of the TPSA'25 workshop sponsored by ACM SIGPLAN.