POPL 2025 (series) / TPSA 2025 (series) / Theory and Practice of Static Analysis 2025 /
Partial Incorrectness Logic
Tue 21 Jan 2025 11:36 - 11:54 at Patty Cake - Program Logics
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.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
Tue 21 Jan
Displayed 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 |