Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying Tree-Manipulating Programs via CHCs

Marco Faella, Gennaro Parlato

TL;DR

The paper tackles automatic verification of programs manipulating tree-shaped heaps, where unbounded growth and aliasing complicate invariants. It introduces knitted-trees, a compositional encoding that maps a program execution $\pi$ on an input tree $T$ to a data tree $\mathcal{K}=(K,\mu)$ with a backbone and lace that record inputs, outputs, and intermediate configurations. Verification reduces to solving CHC systems $\mathcal{C}_{\mathrm{kt}}(P,m,n)$ and $\mathcal{C}_{\mathrm{ex}}(\mathcal{I})$, with a predicate $\mathbf{Lab}$ capturing exactly the labels that occur in knitted-trees and a link between exit status and memory safety. The MemSafety semi-algorithm uses parameter bounds $(m,n)$ and CHC solving to decide memory safety, iteratively enlarging bounds when necessary; the framework supports modular invariants and can extend to richer properties via symbolic data-tree automata.

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.

Verifying Tree-Manipulating Programs via CHCs

TL;DR

The paper tackles automatic verification of programs manipulating tree-shaped heaps, where unbounded growth and aliasing complicate invariants. It introduces knitted-trees, a compositional encoding that maps a program execution on an input tree to a data tree with a backbone and lace that record inputs, outputs, and intermediate configurations. Verification reduces to solving CHC systems and , with a predicate capturing exactly the labels that occur in knitted-trees and a link between exit status and memory safety. The MemSafety semi-algorithm uses parameter bounds and CHC solving to decide memory safety, iteratively enlarging bounds when necessary; the framework supports modular invariants and can extend to richer properties via symbolic data-tree automata.

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.

Paper Structure

This paper contains 3 sections, 2 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Example.
  3. Preliminaries

Figures (2)

  • Figure 1: Running example.
  • Figure 2: A knitted-tree of the program in Fig. \ref{['fig:running example']} on the input list 1 $\!\rightarrow$ 2 $\!\rightarrow$ 3 $\!\rightarrow$ 4 $\!\rightarrow$ 5 and $\mathit{key} = 3$. Blue numbers below the frames represent positions within the label, while red numbers and arrows refer to the lace.

Theorems & Definitions (2)

  • definition thmcounterdefinition
  • definition thmcounterdefinition