Exact Separation Logic (Extended Version)
Petar Maksimovi\'c, Caroline Cronj\"ager, Andreas L\"o\"ow and, Julian Sutherland, Philippa Gardner

TL;DR
This paper introduces exact separation logic (ESL), a new program logic that combines the strengths of over- and under-approximating logics, enabling comprehensive verification and bug detection in heap-manipulating programs.
Contribution
The paper presents ESL, a fully-verified separation logic compatible with both over- and under-approximating verification, and proves its soundness and function compositionality.
Findings
ESL characterizes all terminating behavior and reachable errors.
Proof of soundness for ESL with mutually recursive functions.
Exploration of abstraction's role in UX reasoning.
Abstract
Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised. We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised, and all established results and errors are…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
