Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell University Graduate School
  3. Cornell Theses and Dissertations
  4. Total Outcome Logic: Unified Reasoning For Nontermination and Branching Effects

Total Outcome Logic: Unified Reasoning For Nontermination and Branching Effects

File(s)
Li_cornell_0058O_12572.pdf (477.81 KB)
Permanent Link(s)
https://doi.org/10.7298/sxsm-3458
https://hdl.handle.net/1813/120729
Collections
Cornell Theses and Dissertations
Author
Li, James
Abstract

Since their inception in the form of Hoare Logic, program logics have evolvedfar beyond simple imperative programs, expanding to handle memory along- side additional computational effects such as nondeterminism and probabilistic branching. Orthogonally, more recent research has taken a turn toward incor- rectness logics, which prove the presence of bugs rather than their absence, of- fering greater tractability for industrial adoption. However, correctness and incorrectness reasoning have remained funda- mentally incompatible, forcing practitioners to use separate frameworks. This gap was filled by the recently developed Outcome Logic. By decomposing reasoning on the reachability of separate program outcomes, Outcome Logic was able to unify both paradigms as well as generalize across different branch- ing effects. Our work extends Outcome Logic to address one of its blind spots: namely, reasoning about program (non)termination. While specialized logics exist for termination criteria like partial correctness (termination not assured) and total correctness (guaranteed termination), Outcome Logic can only express partial correctness and its dual—guaranteed divergence. In particular, the semantics of Outcome Logic captures only terminating outcomes, precluding reasoning on nonterminating behavior. We expand the syntax, semantics, and proof rules of Outcome Logic to ex- press the full spectrum of termination conditions of programs. As we will see, the mixture of nontermination and nondeterminism requires a nontrivial re- working of the program semantics. Our resulting framework is shown to be sound and relatively complete, as well as expressive enough to subsume re- cently proposed taxonomies of modern program logics. As a proof of concept, we provide case studies demonstrating the ability to perform different kinds of termination analyses in our logic.

Description
123 pages
Date Issued
2025-08
Committee Chair
Martins da Silva, Alexandra
Committee Member
Hodes, Harold
Degree Discipline
Computer Science
Degree Name
M.S., Computer Science
Degree Level
Master of Science
Type
dissertation or thesis

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance