POPL 2025 (series) / TPSA 2025 (series) / Theory and Practice of Static Analysis 2025 /
Partial Incorrectness Logic
We investigate \emph{partial incorrectness logic}, a program logic related to O’Hearn’s incorrectness logic, analogous to the relationship between partial and total correctness in \emph{Hoare logic} (HL). Whereas partial correctness in HL allows divergence, partial \emph{incorrectness} permits unreachability. Using Dijkstra’s \emph{predicate transformers}, we examine this duality between divergence and unreachability. Further, we provide several examples for applications of partial incorrectness logic.