Projects per year
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 nonlinearity  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 language  English 

Title of host publication  Proceedings of the Third International Workshop on Verification and Program Transformation 
Editors  Alexei Lisitsa, Andrei P. Nemytykh, Alberto Pettorossi 
Number of pages  14 
Place of Publication  London 
Publisher  EPTCS 
Publication date  7 Dec 2015 
Pages  114 
Commissioning body  IMDEA Software Institute 
DOIs  
Publication status  Published  7 Dec 2015 
Event  Third International Workshop on Verification and Program Transformation  London, United Kingdom Duration: 11 Apr 2015 → … https://arxiv.org/html/1512.02215 
Workshop
Workshop  Third International Workshop on Verification and Program Transformation 

Country/Territory  United Kingdom 
City  London 
Period  11/04/2015 → … 
Internet address 
Series  Electronic Proceedings in Theoretical Computer Science 

Volume  199 
ISSN  20752180 
Keywords
 Tree dimension
 proof decomposition
 program transformation
 Horn clauses
Projects
 2 Finished


ENTRA: WholeSystems Energy Transparency
Gallagher, J. P., Rosendahl, M., Rhiger, M., Strand, D. L. & Bohr, N.
01/10/2012 → 30/09/2015
Project: Research