A Theory of Heap for Constrained Horn Clauses (Extended Technical Report)

TL;DR

This paper introduces a new SMT-LIB theory of heap tailored for Constrained Horn Clauses to improve the representation and solving of heap-allocated data structures in verification tools.

Contribution

It presents a formal theory of heap for CHCs, enabling a standard, language-independent way to encode heap data structures in verification.

Findings

Defines syntax and semantics of the heap theory

Reduces heap theory to SMT-LIB arrays and data-types

Discusses properties and potential extensions

Abstract

Constrained Horn Clauses (CHCs) are an intermediate program representation that can be generated by several verification tools, and that can be processed and solved by a number of Horn solvers. One of the main challenges when using CHCs in verification is the encoding of heap-allocated data-structures: such data-structures are today either represented explicitly using the theory of arrays, or transformed away with the help of invariants or refinement types, defeating the purpose of CHCs as a representation that is language-independent as well as agnostic of the algorithm implemented by the Horn solver. This paper presents an SMT-LIB theory of heap tailored to CHCs, with the goal of enabling a standard interchange format for programs with heap data-structures. We introduce the syntax of the theory of heap, define its semantics in terms of axioms and using a reduction to SMT-LIB arrays and data-types, and discuss its properties and outline possible extensions and future work.