### Resumé

interpretation to compute a model of a query-answer transformation of a given set of clauses and a goal. The effect is to propagate the

constraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; we

use the constraints from the model to compute a specialised version of each clause in the program. The approach is independent of

the abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effective

transformation, both in our own verification tools (convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.

Originalsprog | Engelsk |
---|---|

Titel | Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15 |

Redaktører | Kenichi Asai, Kostis Sagonas |

Antal sider | 6 |

Udgivelses sted | New York |

Forlag | Association for Computing Machinery |

Publikationsdato | 4 jan. 2015 |

Sider | 85-90 |

ISBN (Trykt) | 978-1-4503-3297-2 |

DOI | |

Status | Udgivet - 4 jan. 2015 |

Begivenhed | PEPM 2015 - Tata Institute of Fundamental Research, Mumbai, Indien Varighed: 13 jan. 2015 → 14 jan. 2015 http://popl.mpi-sws.org/2015/ |

### Konference

Konference | PEPM 2015 |
---|---|

Lokation | Tata Institute of Fundamental Research |

Land | Indien |

By | Mumbai |

Periode | 13/01/2015 → 14/01/2015 |

Andet | In cooperation with: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages |

Internetadresse |

### Emneord

### Citer dette

*Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15*(s. 85-90). New York: Association for Computing Machinery. https://doi.org/10.1145/2678015.2682544

}

*Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15.*Association for Computing Machinery, New York, s. 85-90, Mumbai, Indien, 13/01/2015. https://doi.org/10.1145/2678015.2682544

**Constraint Specialisation in Horn Clause Verification.** / Kafle, Bishoksan; Gallagher, John Patrick.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - Constraint Specialisation in Horn Clause Verification

AU - Kafle, Bishoksan

AU - Gallagher, John Patrick

N1 - @inproceedings{DBLP:conf/pepm/KafleG15, author = {Bishoksan Kafle and John P. Gallagher}, title = {Constraint Specialisation in Horn Clause Verification}, booktitle = {Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015}, pages = {85--90}, year = {2015}, crossref = {DBLP:conf/pepm/2015}, url = {http://doi.acm.org/10.1145/2678015.2682544}, doi = {10.1145/2678015.2682544}, timestamp = {Sun, 04 Jan 2015 11:56:22 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/KafleG15}, bibsource = {dblp computer science bibliography, http://dblp.org} } @proceedings{DBLP:conf/pepm/2015, editor = {Kenichi Asai and Kostis Sagonas}, title = {Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015}, publisher = {{ACM}}, year = {2015}, url = {http://dl.acm.org/citation.cfm?id=2678015}, isbn = {978-1-4503-3297-2}, timestamp = {Sun, 04 Jan 2015 11:54:44 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/2015}, bibsource = {dblp computer science bibliography, http://dblp.org} }

PY - 2015/1/4

Y1 - 2015/1/4

N2 - We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstractinterpretation to compute a model of a query-answer transformation of a given set of clauses and a goal. The effect is to propagate theconstraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; weuse the constraints from the model to compute a specialised version of each clause in the program. The approach is independent ofthe abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effectivetransformation, both in our own verification tools (convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.

AB - We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstractinterpretation to compute a model of a query-answer transformation of a given set of clauses and a goal. The effect is to propagate theconstraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; weuse the constraints from the model to compute a specialised version of each clause in the program. The approach is independent ofthe abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effectivetransformation, both in our own verification tools (convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.

KW - constraint specialisation

KW - query-answer transformation

KW - Horn clauses

KW - abstract interpretation

U2 - 10.1145/2678015.2682544

DO - 10.1145/2678015.2682544

M3 - Article in proceedings

SN - 978-1-4503-3297-2

SP - 85

EP - 90

BT - Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15

A2 - Asai, Kenichi

A2 - Sagonas, Kostis

PB - Association for Computing Machinery

CY - New York

ER -