Decomposition by tree dimension in Horn clause verification

TL;DR

This paper explores using tree dimension to decompose Horn clause verification problems, enabling parallel proof strategies and potentially improving verification efficiency by analyzing derivation tree complexity.

Contribution

It introduces a novel approach of decomposing Horn clause verification based on tree dimension, facilitating parallel proofs and new insights into derivation tree complexity.

Findings

Preliminary results suggest the approach is promising for proof decomposition.

Tree dimension-based decomposition can enable parallel verification processes.

Using existing tools to analyze derivation tree dimensions is feasible.

Abstract

In this paper we investigate the use of the concept of tree dimension in Horn clause analysis and verification. The dimension of a tree is a measure of its non-linearity - for example a list of any length has dimension zero while a complete binary tree has dimension equal to its height. We apply this concept to trees corresponding to Horn clause derivations. A given set of Horn clauses P can be transformed into a new set of clauses P=<k, whose derivation trees are the subset of P's derivation trees with dimension at most k. Similarly, a set of clauses P>k can be obtained from P whose derivation trees have dimension at least k + 1. In order to prove some property of all derivations of P, we systematically apply these transformations, for various values of k, to decompose the proof into separate proofs for P=<k and P>k (which could be executed in parallel). We show some preliminary results indicating that decomposition by tree dimension is a potentially useful proof technique. We also investigate the use of existing automatic proof tools to prove some interesting properties about dimension(s) of feasible derivation trees of a given program.