POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
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 Jan

Displayed time zone: Mountain Time (US & Canada) change

11:00 - 12:30
Program LogicsTPSA at Patty Cake
11:00
18m
Talk
Data Structure Abstraction and Incorrectness Separation Logic
TPSA
Andreas Lööw Imperial College London
11:18
18m
Talk
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
TPSA
Conrad Zimmerman Northeastern University, Jenna DiVincenzo (Wise) Purdue University
Pre-print
11:36
18m
Talk
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
18m
Talk
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
18m
Talk
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