Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses

Verifying programs that manipulate tree data structures often requires complex, ad-hoc proofs that are hard to generalize and automate. This paper introduces an automatic technique for analyzing such programs. Our approach combines automata and logics to tackle the challenges posed by diverse tree data structures uniformly. At the core of our methodology is the knitted-tree encoding, which maps a program execution into a tree data structure encapsulating input, output, and intermediate configurations, within a single structure. By leveraging the compositional properties of knitted-trees, we characterize them using constrained Horn clauses (CHCs). This encoding reduces verification to solving CHC satisfiability, benefiting from ongoing advancements in CHC solvers. While we focus on the memory safety problem for illustration, our technique applies broadly to various verification tasks involving tree data structures.