Logo: to the web site of Uppsala University

A common approach in software verification is to encode a program as a set of Constrained Horn Clauses (CHCs), which are then processed and solved automatically by a CHC solver. To streamline this verification approach for the case of programs operating on mutable linked data-structures, we have in earlier work proposed a theory of heaps, defined within the SMT-LIB framework, which enables us to represent programs as CHCs with minimal loss of structural information. By preserving high-level program information in the encoding, the theory of heaps enables CHC solvers to apply various internal techniques for handling program heap; among others, to encode the heap further using the theory of arrays, to apply shape analysis, or to translate to a heap-less program with the help of invariants. This paper explores the third option, developing transformation rules that rewrite a set of CHCs into an equisatisfiable set of CHCs with additional predicates representing heap invariants. The proposed method generalises the notion of space invariants, which were previously introduced for verifying Java programs, by lifting the entire transformation process to the CHC level. The paper defines the transformation rules, provides detailed correctness proofs, and discusses the strengths and limitations of the approach. We also outline possible extensions of the method.