Tree dimension in verification of constrained Horn clauses

Bishoksan Kafle, John Patrick Gallagher, Pierre Ganty

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

In 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 CHCs P, we define a transformation of P yielding a dimension bounded set of CHCs P≤k. The set of derivations for P≤k consists of the derivations for P that have dimension at most k. We also show how to construct a set of clauses denoted P>k whose derivations have dimension exceeding k. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.
Originalsprog Engelsk Theory and Practice of Logic Programming 18 2 224-251 1471-0684 https://doi.org/10.1017/S1471068418000030 Udgivet - 2018

Citer dette

@article{1a32a77d2f924288b037a7e4e429d677,
title = "Tree dimension in verification of constrained Horn clauses",
abstract = "In 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 CHCs P, we define a transformation of P yielding a dimension bounded set of CHCs P≤k. The set of derivations for P≤k consists of the derivations for P that have dimension at most k. We also show how to construct a set of clauses denoted P>k whose derivations have dimension exceeding k. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.",
keywords = "program ver, program analysis, Logic Programming",
author = "Bishoksan Kafle and Gallagher, {John Patrick} and Pierre Ganty",
year = "2018",
doi = "10.1017/S1471068418000030",
language = "English",
volume = "18",
pages = "224--251",
journal = "Theory and Practice of Logic Programming",
issn = "1471-0684",
publisher = "Cambridge University Press",
number = "2",

}

Tree dimension in verification of constrained Horn clauses. / Kafle, Bishoksan; Gallagher, John Patrick; Ganty, Pierre.

I: Theory and Practice of Logic Programming, Bind 18, Nr. 2, 2018, s. 224-251.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Tree dimension in verification of constrained Horn clauses

AU - Kafle, Bishoksan

AU - Gallagher, John Patrick

AU - Ganty, Pierre

PY - 2018

Y1 - 2018

N2 - In 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 CHCs P, we define a transformation of P yielding a dimension bounded set of CHCs P≤k. The set of derivations for P≤k consists of the derivations for P that have dimension at most k. We also show how to construct a set of clauses denoted P>k whose derivations have dimension exceeding k. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.

AB - In 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 CHCs P, we define a transformation of P yielding a dimension bounded set of CHCs P≤k. The set of derivations for P≤k consists of the derivations for P that have dimension at most k. We also show how to construct a set of clauses denoted P>k whose derivations have dimension exceeding k. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.

KW - program ver

KW - program analysis

KW - Logic Programming

U2 - 10.1017/S1471068418000030

DO - 10.1017/S1471068418000030

M3 - Journal article

VL - 18

SP - 224

EP - 251

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

SN - 1471-0684

IS - 2

ER -