Journal article

Tree dimension in verification of constrained Horn clauses

B Kafle, JP Gallagher, P Ganty

Theory and Practice of Logic Programming | Published : 2018


AbstractIn this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCsP, we define a transformation ofPyielding adimension-boundedset of CHCsP≤k. The set of der..

View full abstract

Citation metrics