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

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 |

Udgivelses sted | London |

Forlag | EPTCS |

Publikationsdato | 7 dec. 2015 |

Sider | 1-14 |

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 | Storbritannien |

By | London |

Periode | 11/04/2015 → … |

Internetadresse |

Navn | Electronic Proceedings in Theoretical Computer Science |
---|---|

Vol/bind | 199 |

ISSN | 2075-2180 |

## Projekter

- 2 Afsluttet

## ICT-Energy

Gallagher, J. P., Rosendahl, M. & Bohr, N.

01/10/2013 → 30/09/2016

Projekter: Projekt › Forskning

## ENTRA: Whole-Systems Energy Transparency

Gallagher, J. P., Rosendahl, M., Rhiger, M., Strand, D. L. & Bohr, N.

01/10/2012 → 30/09/2015

Projekter: Projekt › Forskning

## Citer dette

Kafle, B., Gallagher, J. P., & Ganty, P. (2015). Decomposition by tree dimension in Horn clause verification. I A. Lisitsa, A. P. Nemytykh, & A. Pettorossi (red.),

*Proceedings of the Third International Workshop on Verification and Program Transformation*(s. 1-14). EPTCS. Electronic Proceedings in Theoretical Computer Science, Bind. 199 https://doi.org/10.4204/EPTCS.199