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