Decomposition by tree dimension in Horn clause verification

Bishoksan Kafle, John Patrick Gallagher, Pierre Ganty

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.
Original languageEnglish
Title of host publicationProceedings of the Third International Workshop on Verification and Program Transformation
EditorsAlexei Lisitsa, Andrei P. Nemytykh, Alberto Pettorossi
Number of pages14
Place of PublicationLondon
PublisherEPTCS
Publication date7 Dec 2015
Pages1-14
Commissioning bodyIMDEA Software Institute
DOIs
Publication statusPublished - 7 Dec 2015
EventThird International Workshop on Verification and Program Transformation - London, United Kingdom
Duration: 11 Apr 2015 → …
https://arxiv.org/html/1512.02215

Workshop

WorkshopThird International Workshop on Verification and Program Transformation
CountryUnited Kingdom
CityLondon
Period11/04/2015 → …
Internet address
SeriesElectronic Proceedings in Theoretical Computer Science
Volume199
ISSN2075-2180

Keywords

  • Tree dimension
  • proof decomposition
  • program transformation
  • Horn clauses

Cite this

Kafle, B., Gallagher, J. P., & Ganty, P. (2015). Decomposition by tree dimension in Horn clause verification. In A. Lisitsa, A. P. Nemytykh, & A. Pettorossi (Eds.), Proceedings of the Third International Workshop on Verification and Program Transformation (pp. 1-14). London: EPTCS. Electronic Proceedings in Theoretical Computer Science, Vol.. 199 https://doi.org/10.4204/EPTCS.199
Kafle, Bishoksan ; Gallagher, John Patrick ; Ganty, Pierre. / Decomposition by tree dimension in Horn clause verification. Proceedings of the Third International Workshop on Verification and Program Transformation. editor / Alexei Lisitsa ; Andrei P. Nemytykh ; Alberto Pettorossi. London : EPTCS, 2015. pp. 1-14 (Electronic Proceedings in Theoretical Computer Science, Vol. 199).
@inproceedings{a2b6733d2fc44086bdaf2d51889ff216,
title = "Decomposition by tree dimension in Horn clause verification",
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 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 (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.",
keywords = "Tree dimension, proof decomposition, program transformation, Horn clauses",
author = "Bishoksan Kafle and Gallagher, {John Patrick} and Pierre Ganty",
year = "2015",
month = "12",
day = "7",
doi = "10.4204/EPTCS.199",
language = "English",
pages = "1--14",
editor = "Alexei Lisitsa and Nemytykh, {Andrei P.} and Alberto Pettorossi",
booktitle = "Proceedings of the Third International Workshop on Verification and Program Transformation",
publisher = "EPTCS",

}

Kafle, B, Gallagher, JP & Ganty, P 2015, Decomposition by tree dimension in Horn clause verification. in A Lisitsa, AP Nemytykh & A Pettorossi (eds), Proceedings of the Third International Workshop on Verification and Program Transformation. EPTCS, London, Electronic Proceedings in Theoretical Computer Science, vol. 199, pp. 1-14, Third International Workshop on Verification and Program Transformation , London, United Kingdom, 11/04/2015. https://doi.org/10.4204/EPTCS.199

Decomposition by tree dimension in Horn clause verification. / Kafle, Bishoksan; Gallagher, John Patrick; Ganty, Pierre.

Proceedings of the Third International Workshop on Verification and Program Transformation. ed. / Alexei Lisitsa; Andrei P. Nemytykh; Alberto Pettorossi. London : EPTCS, 2015. p. 1-14.

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Decomposition by tree dimension in Horn clause verification

AU - Kafle, Bishoksan

AU - Gallagher, John Patrick

AU - Ganty, Pierre

PY - 2015/12/7

Y1 - 2015/12/7

N2 - 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 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 (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.

AB - 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 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 (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.

KW - Tree dimension

KW - proof decomposition

KW - program transformation

KW - Horn clauses

U2 - 10.4204/EPTCS.199

DO - 10.4204/EPTCS.199

M3 - Article in proceedings

SP - 1

EP - 14

BT - Proceedings of the Third International Workshop on Verification and Program Transformation

A2 - Lisitsa, Alexei

A2 - Nemytykh, Andrei P.

A2 - Pettorossi, Alberto

PB - EPTCS

CY - London

ER -

Kafle B, Gallagher JP, Ganty P. Decomposition by tree dimension in Horn clause verification. In Lisitsa A, Nemytykh AP, Pettorossi A, editors, Proceedings of the Third International Workshop on Verification and Program Transformation. London: EPTCS. 2015. p. 1-14. (Electronic Proceedings in Theoretical Computer Science, Vol. 199). https://doi.org/10.4204/EPTCS.199