POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

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.