Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses

TL;DR

This paper presents an automated verification method for tree-manipulating programs by encoding program executions as knitted-trees and reducing verification to solving constrained Horn clauses, enabling broader application and automation.

Contribution

It introduces a novel knitted-tree encoding and a CHC-based verification approach for programs manipulating complex tree data structures.

Findings

Effective encoding of program executions as knitted-trees

Reduction of verification to CHC satisfiability

Broad applicability to various verification tasks involving trees

Abstract

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.