A Stricter Heap Separating Points-To Logic
Ren\'e Haberland, Kirill Krinkin

TL;DR
This paper introduces a more rigorous approach to heap separation logic, enhancing the formal verification of dynamic memory behavior in programs to better detect and prevent memory issues.
Contribution
It proposes a stricter heap separating points-to logic, improving the precision and reliability of heap memory verification compared to existing methods.
Findings
Enhanced formal verification of heap memory behavior
More accurate detection of memory issues
Improved reasoning about heap graph structures
Abstract
Dynamic memory issues are hard to locate and may cost much of a development project's efforts and was repeatedly reported similarly afterwards independently by different persons. Verification as one formal method may proof a given program's heap matches a specified dynamic behaviour. Dynamic (or heap) memory, is the region within main memory that is manipulated by program statements like alloc, free and pointer manipulation during program execution. Usually, heap memory is allocated for problems where the amount of used memory is unknown prior to execution. Regions within the heap may be related "somehow" with each other, often, but not always, by pointers containing absolute addresses of related heap cells. The data structure described by all valid pointer variables manifests heap graphs. A heap graph is a directed connected simple graph within the dynamic memory which may contain…
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.
Taxonomy
TopicsLogic, programming, and type systems · Software Testing and Debugging Techniques · Formal Methods in Verification
