Incorrectness Separation Logic with Arrays and Pointer Arithmetic
Yeonseok Lee, Koji Nakazawa
TL;DR
This paper extends Incorrectness Separation Logic (ISL) to support variable-length array predicates and pointer arithmetic, enabling precise bug-finding in heap-manipulating programs that manipulate arrays. It achieves this by defining a weakest postcondition framework $\textsf{WPO}[\![P,\mathbb{C},\epsilon]\!]$ and a corresponding generating function $\textsf{wpo}$ to compute postconditions for heap operations, while employing a block-based memory model and canonical forms to handle arithmetic and array predicates. The authors prove the relative completeness of the extended ISL by demonstrating the expressiveness of $\textsf{wpo}$ and showing that every valid ISL triple is derivable from $[P]\;\mathbb{C}\;[\epsilon:\;\textsf{wpo}(P,\mathbb{C},\epsilon)]$. This work connects ISL with existing array-separation logic research and sets the stage for future automation improvements, while highlighting the trade-off between expressiveness and the complexity of the proof rules.
Abstract
Incorrectness Separation Logic (ISL) is a proof system designed to automate verification and detect bugs in programs manipulating heap memories. In this study, we extend ISL to support variable-length array predicates and pointer arithmetic. Additionally, we prove the relative completeness of this extended ISL by constructing the weakest postconditions. Relative completeness means that all valid ISL triples are provable, assuming an oracle capable of checking entailment between formulas; this property ensures the reliability of the proof system.