Incorrectness Separation Logic with Arrays and Pointer Arithmetic
Logic in Computer Science
2025-03-04 v1
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.
Cite
@article{arxiv.2503.00809,
title = {Incorrectness Separation Logic with Arrays and Pointer Arithmetic},
author = {Yeonseok Lee and Koji Nakazawa},
journal= {arXiv preprint arXiv:2503.00809},
year = {2025}
}
Comments
47 pages, 6 figures