Name
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.4204/EPTCS.199.1 | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE |
Keywords | DocType | Issue |
Tree dimension, proof decomposition, program transformation, Horn clauses | Journal | 199 |
ISSN | Citations | PageRank |
2075-2180 | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| bishoksan kafle | 1 | 39 | 7.88 |
| John P. Gallagher | 2 | 984 | 59.94 |
| Pierre Ganty | 3 | 242 | 20.29 |