### Resumé

Sprog | Engelsk |
---|---|

Tidsskrift | Science of Computer Programming |

Vol/bind | 137 |

Sider | 125-140 |

ISSN | 0167-6423 |

DOI | |

Status | Udgivet - 1 apr. 2017 |

### Emneord

### Citer dette

*Science of Computer Programming*,

*137*, 125-140. DOI: 10.1016/j.scico.2017.01.002

}

*Science of Computer Programming*, bind 137, s. 125-140. DOI: 10.1016/j.scico.2017.01.002

**Constraint specialisation in Horn clause verification.** / Kafle, Bishoksan; Gallagher, John Patrick.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel

TY - JOUR

T1 - Constraint specialisation in Horn clause verification

AU - Kafle,Bishoksan

AU - Gallagher,John Patrick

PY - 2017/4/1

Y1 - 2017/4/1

N2 - We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstract interpretation to compute a model of a query–answer transformed version of a given set of clauses and a goal. The constraints from the model are then used to compute a specialised version of each clause. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. The specialisation procedure can be repeated to yield further specialisation. The approach is independent of the abstract domain and the constraint theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (based on a 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 abstract interpretation to compute a model of a query–answer transformed version of a given set of clauses and a goal. The constraints from the model are then used to compute a specialised version of each clause. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. The specialisation procedure can be repeated to yield further specialisation. The approach is independent of the abstract domain and the constraint theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (based on a convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.

KW - Constraint specialisation

KW - Query–answer transformation

KW - Program verification

KW - program analysis

KW - Abstract Interpretation

U2 - 10.1016/j.scico.2017.01.002

DO - 10.1016/j.scico.2017.01.002

M3 - Journal article

VL - 137

SP - 125

EP - 140

JO - Science of Computer Programming

T2 - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

ER -