### Abstract

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 | 1-14 |

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 | United Kingdom |

City | London |

Period | 11/04/2015 → … |

Internet address |

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

Volume | 199 |

ISSN | 2075-2180 |

### Keywords

- Tree dimension
- proof decomposition
- program transformation
- Horn clauses

### Cite this

*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

}

*Proceedings of the Third International Workshop on Verification and Program Transformation.*EPTCS, London, Electronic Proceedings in Theoretical Computer Science, vol. 199, pp. 1-14, Third International Workshop on Verification and Program Transformation , London, United Kingdom, 11/04/2015. https://doi.org/10.4204/EPTCS.199

**Decomposition by tree dimension in Horn clause verification.** / Kafle, Bishoksan; Gallagher, John Patrick; Ganty, Pierre.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Decomposition by tree dimension in Horn clause verification

AU - Kafle, Bishoksan

AU - Gallagher, John Patrick

AU - Ganty, Pierre

PY - 2015/12/7

Y1 - 2015/12/7

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

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

KW - Tree dimension

KW - proof decomposition

KW - program transformation

KW - Horn clauses

U2 - 10.4204/EPTCS.199

DO - 10.4204/EPTCS.199

M3 - Article in proceedings

SP - 1

EP - 14

BT - Proceedings of the Third International Workshop on Verification and Program Transformation

A2 - Lisitsa, Alexei

A2 - Nemytykh, Andrei P.

A2 - Pettorossi, Alberto

PB - EPTCS

CY - London

ER -