Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching
While there is a long tradition of reasoning about termination (and nontermination) in the context of program analysis, specialized logics are typically needed to give different termination guarantees. This includes partial correctness, where termination is not guaranteed; total correctness, where it is guaranteed; and newer logics for explicitly proving \emph{nontermination}. We present \emph{Total Outcome Logic}, a single logic which can express the full spectrum of termination conditions and program properties offered by the aforementioned logics.
Total Outcome Logic extends termination and incorrectness reasoning across different kinds of branching effects, so that a single metatheory powers this reasoning in different kinds of programs, including those with nondeterminism and randomization.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:30 | |||
11:00 18mTalk | Data Structure Abstraction and Incorrectness Separation Logic TPSA Andreas Lööw Imperial College London | ||
11:18 18mTalk | Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification TPSA Pre-print | ||
11:36 18mTalk | Partial Incorrectness Logic TPSA Lena Verscht RWTH Aachen University; Saarland University, Ānrán Wáng Saarland University, Benjamin Lucien Kaminski Saarland University; University College London | ||
11:54 18mTalk | Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching TPSA James Li Cornell University, Noam Zilberstein Cornell University, Alexandra Silva Cornell University | ||
12:12 18mTalk | U-turn: Forward-driven backward analysis for incorrectness TPSA Flavio Ascari University of Pisa, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Azalea Raad Imperial College London | ||