A Logical Programming Language as an Instrument for Specifying and Verifying Dynamic Memory

TL;DR

This paper introduces a Prolog-based language for specifying and verifying dynamic memory in programs, focusing on formal verification methods within a Hoare calculus framework to address common heap-related issues.

Contribution

It presents a novel Prolog dialect for formal specification and verification of dynamic memory, emphasizing heap properties and addressing unresolved heap problems in programming.

Findings

Identifies key heap issues like invalid assignment and excessive allocation.

Proposes a formal verification approach using Hoare calculus.

Highlights ongoing challenges in heap management and verification.

Abstract

This work proposes a Prolog-dialect for the found and prioritised problems on expressibility and automation. Given some given C-like program, if dynamic memory is allocated, altered and freed on runtime, then a description of desired dynamic memory is a heap specification. The check of calculated memory state against a given specification is dynamic memory verification. This contribution only considers formal specification and verification in a Hoare calculus. Issues found include: invalid assignment, (temporary) unavailable data in memory cells, excessive memory allocation, (accidental) heap alteration in unexpected regions and others. Excessive memory allocation is nowadays successfully resolved by memory analysers like Valgrind. Essentially, papers in those areas did not bring any big breakthrough. Possible reasons may also include the decrease of tension due to more available memory and parallel threads. However, starting with Apt, problems related to variable modes have not yet been resolved -- neither entirely nor in an acceptable way. Research contributions over the last decades show again and again that heap issues remain and remain complex and still important. A significant contribution was reached in 2016 by Peter O'Hearn, who accepted the G\"{o}del prize for his parallel approach on a spatial heap operation.