Abstract
| Original language | English |
|---|---|
| Title of host publication | Proceedings First Workshop on Horn Clauses for Verification and Synthesis |
| Editors | Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko, Valerio Senni |
| Number of pages | 15 |
| Volume | 169 |
| Publisher | EPTCS |
| Publication date | 2 Dec 2014 |
| Pages | 53-67 |
| Article number | 7 |
| DOIs | |
| Publication status | Published - 2 Dec 2014 |
| Event | First Workshop on Horn Clauses for Verification and Synthesis - Vienna, Austria Duration: 17 Jul 2014 → 17 Jul 2014 |
Conference
| Conference | First Workshop on Horn Clauses for Verification and Synthesis |
|---|---|
| Country | Austria |
| City | Vienna |
| Period | 17/07/2014 → 17/07/2014 |
Keywords
- constrained Horn clause
- convex polyhedral abstraction
- specialisation
Cite this
}
Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification. / Kafle, Bishoksan; Gallagher, John Patrick.
Proceedings First Workshop on Horn Clauses for Verification and Synthesis. ed. / Nikolaj Bjørner; Fabio Fioravanti; Andrey Rybalchenko; Valerio Senni. Vol. 169 EPTCS, 2014. p. 53-67 7.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
TY - GEN
T1 - Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
AU - Kafle, Bishoksan
AU - Gallagher, John Patrick
PY - 2014/12/2
Y1 - 2014/12/2
N2 - We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a domain of convex polyhedra, specialisation of the constraints in CHCs using abstract interpretation of query-answer transformed clauses, and refinement by splitting predicates. The purpose of the work is to investigate how analysis and transformation tools developed for constraint logic programs (CLP) can be applied to the Horn clause verification problem. Abstract interpretation over convex polyhedra is capable of deriving sophisticated invariants and when used in conjunction with specialisation for propagating constraints it can frequently solve challenging verification problems. This is a contribution in itself, but refinement is needed when it fails, and the question of how to refine convex polyhedral analyses has not been studied much. We present a refinement technique based on interpolants derived from a counterexample trace; these are used to drive a property-based specialisation that splits predicates, leading in turn to more precise convex polyhedral analyses. The process of specialisation, analysis and splitting can be repeated, in a manner similar to the CEGAR and iterative specialisation approaches.
AB - We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a domain of convex polyhedra, specialisation of the constraints in CHCs using abstract interpretation of query-answer transformed clauses, and refinement by splitting predicates. The purpose of the work is to investigate how analysis and transformation tools developed for constraint logic programs (CLP) can be applied to the Horn clause verification problem. Abstract interpretation over convex polyhedra is capable of deriving sophisticated invariants and when used in conjunction with specialisation for propagating constraints it can frequently solve challenging verification problems. This is a contribution in itself, but refinement is needed when it fails, and the question of how to refine convex polyhedral analyses has not been studied much. We present a refinement technique based on interpolants derived from a counterexample trace; these are used to drive a property-based specialisation that splits predicates, leading in turn to more precise convex polyhedral analyses. The process of specialisation, analysis and splitting can be repeated, in a manner similar to the CEGAR and iterative specialisation approaches.
KW - constrained Horn clause
KW - convex polyhedral abstraction
KW - specialisation
U2 - 10.4204/EPTCS.169.7
DO - 10.4204/EPTCS.169.7
M3 - Article in proceedings
VL - 169
SP - 53
EP - 67
BT - Proceedings First Workshop on Horn Clauses for Verification and Synthesis
A2 - Bjørner, Nikolaj
A2 - Fioravanti, Fabio
A2 - Rybalchenko, Andrey
A2 - Senni, Valerio
PB - EPTCS
ER -