Decomposition by tree dimension in Horn clause verification

Bishoksan Kafle
(Roskilde University, Denmark)
John P. Gallagher
(Roskilde University, Denmark and IMDEA Software Institute, Spain)
Pierre Ganty
(IMDEA Software Institute, Spain)

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.

In Alexei Lisitsa, Andrei P. Nemytykh and Alberto Pettorossi: Proceedings of the Third International Workshop on Verification and Program Transformation (VPT 2015), London, United Kingdom, 11th April 2015, Electronic Proceedings in Theoretical Computer Science 199, pp. 1–14.
Published: 7th December 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.199.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org