A Stricter Heap Separating Points-To Logic

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 cycles, and where each vertex represents an unique memory address and every edge links two heap vertices. The heap graph must be pointed by at least one variable from the local stack or a chain of other heap graphs which is finally pointed by at least one stacked variable. Heap vertices may not overlap. A heap formula expresses the assertion on dynamic memory and can either be a heaplet, or a recursively defined heap-spatial or logical formula.