U-turn: Forward-driven backward analysis for incorrectness
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 JanDisplayed 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 |