Verifying Tree-Manipulating Programs via CHCs

TL;DR

This paper presents a unified method for verifying programs that manipulate tree data structures by encoding their execution as constrained Horn clauses, simplifying the verification process.

Contribution

It introduces the knitted-tree encoding and demonstrates how to verify tree-manipulating programs using CHC satisfiability, enabling modular and automated proofs.

Findings

Effective encoding of tree manipulations as CHCs

Simplified verification of memory safety in tree programs

Modular invariants derived from the approach

Abstract

Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, foundational approach to verifying such programs. Central to our approach is the knitted-tree encoding, modeling each program execution as a tree structure capturing input, output, and intermediate states. Leveraging the compositional nature of knitted-trees, we encode these structures as constrained Horn clauses (CHCs), reducing verification to CHC satisfiability task. To illustrate our approach, we focus on memory safety and show how it naturally leads to simple, modular invariants.