2 papers
cs.LO2025
Relative Completeness of Incorrectness Separation Logic
Yeonseok Lee, Koji Nakazawa
Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily…
cs.LO2025
Incorrectness Separation Logic with Arrays and Pointer Arithmetic
Yeonseok Lee, Koji Nakazawa
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 sup…