REVIEW 1 cited by
Total Outcome Logic: Unified Reasoning for a Taxonomy of Program Logics
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
While there is a long tradition of reasoning about (non)termination in program analysis, specialized logics are typically needed to give different termination criteria. This includes partial correctness, where termination is not guaranteed, and total correctness, where it is guaranteed. We present Total Outcome Logic (TOL), a single logic which can express the full spectrum of termination conditions and program properties offered by the aforementioned logics. TOL extends (non)termination and (in)correctness reasoning across different kinds of branching effects, so that a single metatheory powers this reasoning in different kinds of programs, including nondeterministic and probabilistic. We also show that TOL subsumes several recently created taxonomies of (in)correctness logics, so that many different kinds of properties can be proven with a single unified theory.
Forward citations
Cited by 1 Pith paper
-
Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary
opOL is a Hoare-style logic with priv/leak outcome assertions and a Frame rule that stays sound under oblivious adversaries by treating adversarial schedule consumption as a separation-logic resource.
Discussion (0). Continue with ORCID to comment.