Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification

Bishoksan Kafle, John Patrick Gallagher

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

Resumé

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.
OriginalsprogEngelsk
TitelProceedings First Workshop on Horn Clauses for Verification and Synthesis
RedaktørerNikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko, Valerio Senni
Antal sider15
Vol/bind169
ForlagEPTCS
Publikationsdato2 dec. 2014
Sider53-67
Artikelnummer7
DOI
StatusUdgivet - 2 dec. 2014
BegivenhedFirst Workshop on Horn Clauses for Verification and Synthesis - Vienna, Østrig
Varighed: 17 jul. 201417 jul. 2014

Konference

KonferenceFirst Workshop on Horn Clauses for Verification and Synthesis
LandØstrig
ByVienna
Periode17/07/201417/07/2014

Citer dette

Kafle, B., & Gallagher, J. P. (2014). Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification. I N. Bjørner, F. Fioravanti, A. Rybalchenko, & V. Senni (red.), Proceedings First Workshop on Horn Clauses for Verification and Synthesis (Bind 169, s. 53-67). [7] EPTCS. https://doi.org/10.4204/EPTCS.169.7
Kafle, Bishoksan ; Gallagher, John Patrick. / Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification. Proceedings First Workshop on Horn Clauses for Verification and Synthesis. red. / Nikolaj Bjørner ; Fabio Fioravanti ; Andrey Rybalchenko ; Valerio Senni. Bind 169 EPTCS, 2014. s. 53-67
@inproceedings{5c72f88fd0934c8192c8cad970b09adf,
title = "Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification",
abstract = "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.",
keywords = "constrained Horn clause, convex polyhedral abstraction, specialisation",
author = "Bishoksan Kafle and Gallagher, {John Patrick}",
year = "2014",
month = "12",
day = "2",
doi = "10.4204/EPTCS.169.7",
language = "English",
volume = "169",
pages = "53--67",
editor = "Nikolaj Bj{\o}rner and Fabio Fioravanti and Andrey Rybalchenko and Valerio Senni",
booktitle = "Proceedings First Workshop on Horn Clauses for Verification and Synthesis",
publisher = "EPTCS",

}

Kafle, B & Gallagher, JP 2014, Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification. i N Bjørner, F Fioravanti, A Rybalchenko & V Senni (red), Proceedings First Workshop on Horn Clauses for Verification and Synthesis. bind 169, 7, EPTCS, s. 53-67, First Workshop on Horn Clauses for Verification and Synthesis , Vienna, Østrig, 17/07/2014. https://doi.org/10.4204/EPTCS.169.7

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. red. / Nikolaj Bjørner; Fabio Fioravanti; Andrey Rybalchenko; Valerio Senni. Bind 169 EPTCS, 2014. s. 53-67 7.

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer 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 -

Kafle B, Gallagher JP. Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification. I Bjørner N, Fioravanti F, Rybalchenko A, Senni V, red., Proceedings First Workshop on Horn Clauses for Verification and Synthesis. Bind 169. EPTCS. 2014. s. 53-67. 7 https://doi.org/10.4204/EPTCS.169.7