HEAP VERIFICATION OF OBJECT-ORIENTED PROGRAMS IN A POINTS-TO LOGIC

In this paper a verification technique is presented based on the logical programming language “PROLOG” for objectoriented programs based on the points-to heap model. The terms “heap”, “heap interpretation” and a heap theory are introduced, and a generalised approach in PROLOG allows to bridge expressibility gaps as well as other research problems in this field as discussed in the paper. The chosen model was validated against [1], which also provides facilities to transform imperative programming languages with objects into an intermediate representation in PROLOG.

Authors: R. Haberland, S. A. Ivanovskiy, K. V. Krinkin

Direction: Informatics and Computer Technologies

Keywords: Pointers, heaps, alias analysis, dynamic memory verification

---

View full article