Verifying Tree-Manipulating Programs via CHCs

2025/05/20 by Marco Faella, Faella, Marco, Gennaro Parlato +1
Computer Science · #F.3.1 #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Software Testing and Debugging Techniques

paper · pdf · doi:10.48550/arxiv.2505.14092

openalex publication_date 2025/05/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• What's Decidable About Program Verification Modulo Axioms?
• Automated Mutual Explicit Induction Proof in Separation Logic
• Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
• The Tree Width of Separation Logic with Recursive Definitions
• Algorithmic Verification of Single-Pass List Processing Programs

Related

• Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
• A data-driven CHC solver
• Sound and Complete Invariant-Based Heap Encodings (Technical Report)
• An encoding of array verification problems into array-free Horn clauses
• RustHorn: CHC-based Verification for Rust Programs