Abstract
| Original language | English |
|---|---|
| Journal | Science of Computer Programming |
| Volume | 137 |
| Pages (from-to) | 125-140 |
| ISSN | 0167-6423 |
| DOIs | |
| Publication status | Published - 1 Apr 2017 |
Keywords
- Constraint specialisation
- Query–answer transformation
- Program verification
- program analysis
- Abstract Interpretation
Cite this
}
Constraint specialisation in Horn clause verification. / Kafle, Bishoksan; Gallagher, John Patrick.
In: Science of Computer Programming, Vol. 137, 01.04.2017, p. 125-140.Research output: Contribution to journal › Journal article › Research › peer-review
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
JF - Science of Computer Programming
SN - 0167-6423
ER -