Decomposition by tree dimension in Horn clause verification

Bishoksan Kafle, John Patrick Gallagher, Pierre Ganty

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review


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.
TitelProceedings of the Third International Workshop on Verification and Program Transformation
RedaktørerAlexei Lisitsa, Andrei P. Nemytykh, Alberto Pettorossi
Antal sider14
Publikationsdato7 dec. 2015
AnsøgerIMDEA Software Institute
StatusUdgivet - 7 dec. 2015
BegivenhedThird International Workshop on Verification and Program Transformation - London, Storbritannien
Varighed: 11 apr. 2015 → …


WorkshopThird International Workshop on Verification and Program Transformation
Periode11/04/2015 → …
NavnElectronic Proceedings in Theoretical Computer Science

Citer dette