On Extending Incorrectness Logic with Backwards Reasoning

Freek Verbeek*, Md Syadus Sefat, Zhoulai Fu, Binoy Ravindran

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

This paper studies an extension of O'Hearn's incorrectness logic (IL) that allows backwards reasoning. IL in its current form does not generically permit backwards reasoning. We show that this can be mitigated by extending IL with underspecification. The resulting logic combines underspecification (the result, or postcondition, only needs to formulate constraints over relevant variables) with underapproximation (it allows to focus on fewer than all the paths). We prove soundness of the proof system, as well as completeness for a defined subset of presumptions. We discuss proof strategies that allow one to derive a presumption from a given result. Notably, we show that the existing concept of loop summaries - closed-form symbolic representations that summarize the effects of executing an entire loop at once - is highly useful. The logic, the proof system and all theorems have been formalized in the Isabelle/HOL theorem prover.

Original languageEnglish
Article number14
Number of pages25
JournalProceedings of the ACM on Programming Languages
Volume9
Issue numberPOPL
DOIs
Publication statusPublished - 7 Jan 2025

Keywords

  • backwards reasoning
  • incorrectness logic
  • program logic

Fingerprint

Dive into the research topics of 'On Extending Incorrectness Logic with Backwards Reasoning'. Together they form a unique fingerprint.

Cite this