Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Watch this 20-minute conference talk from POPL 2025 that explores an extension of O'Hearn's incorrectness logic (IL) to enable backwards reasoning. Learn how researchers Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, and Binoy Ravindran address the limitations of current IL by incorporating underspecification. The presentation explains how this extended logic combines underspecification with underapproximation, allowing developers to focus on fewer paths while only formulating constraints over relevant variables. Discover the soundness and completeness proofs of their system, practical proof strategies for deriving presumptions from results, and how loop summaries can be effectively utilized in this context. The research has been formally verified in the Isabelle/HOL theorem prover, with artifacts available for further exploration. This talk is part of the ACM SIGPLAN POPL 2025 conference held January 19-25, 2025.
