POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Tue 21 Jan 2025 12:12 - 12:30 at Patty Cake - Program Logics

Logics for correctness aim to prove error absence but rely on over-approximations, leading to false alarms that can hamper programmer productivity. Conversely, logics for incorrectness expose true bugs by using under-approximations. We combine forward and backward reasoning for incorrectness: first, a forward analysis using O’Hearn’s Incorrectness Logic (IL) identifies some reachable errors. Then, a backward analysis, led by a new variant of Ascari et al.’s Sufficient Incorrectness Logic (SIL) and guided by IL’s proof tree, reveals the preconditions responsible for errors. Beyond theoretical and practical advances that our proof system can enact for program analysis, we highlight its novel logical judgement format, called UT format (for u-turn), here exemplified for forward-driven backward analysis: we argue that it can be readily adapted to other settings, e.g., to use the SIL proofs to guide the IL inference of reachable errors.

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