2021/04/09 by Zafer Esen, Esen, Zafer, Philipp Rümmer +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2104.04224
openalex publication_date 2021/04/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.