Decomposition By Tree Dimension In Horn Clause Verification
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE(2015)
摘要
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.
更多查看译文
关键词
Tree dimension, proof decomposition, program transformation, Horn clauses
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要