Projekter pr. år
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.
Originalsprog  Engelsk 

Titel  Proceedings of the Third International Workshop on Verification and Program Transformation 
Redaktører  Alexei Lisitsa, Andrei P. Nemytykh, Alberto Pettorossi 
Antal sider  14 
Udgivelsessted  London 
Forlag  EPTCS 
Publikationsdato  7 dec. 2015 
Sider  114 
Ansøger  IMDEA Software Institute 
DOI  
Status  Udgivet  7 dec. 2015 
Begivenhed  Third International Workshop on Verification and Program Transformation  London, Storbritannien Varighed: 11 apr. 2015 → … https://arxiv.org/html/1512.02215 
Workshop
Workshop  Third International Workshop on Verification and Program Transformation 

Land/Område  Storbritannien 
By  London 
Periode  11/04/2015 → … 
Internetadresse 
Navn  Electronic Proceedings in Theoretical Computer Science 

Vol/bind  199 
ISSN  20752180 
Projekter
 2 Afsluttet

ICTEnergy
Gallagher, J. P., Rosendahl, M. & Bohr, N.
01/10/2013 → 30/09/2016
Projekter: Projekt › Forskning

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