Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
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 predica...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1412.1154v1 |
| _version_ | 1811191893979037696 |
|---|---|
| author | Bishoksan Kafle John P. Gallagher |
| author_facet | Bishoksan Kafle John P. Gallagher |
| author_sort | Bishoksan Kafle |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-11T23:44:25Z |
| format | Article |
| id | doaj.art-8f7185a315b9455dad5e13ca33a47a6b |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-11T23:44:25Z |
| publishDate | 2014-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-8f7185a315b9455dad5e13ca33a47a6b2022-12-22T03:56:42ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-12-01169Proc. HCVS 2014536710.4204/EPTCS.169.7:2Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verificationBishoksan KafleJohn P. GallagherWe 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.http://arxiv.org/pdf/1412.1154v1 |
| spellingShingle | Bishoksan Kafle John P. Gallagher Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification Electronic Proceedings in Theoretical Computer Science |
| title | Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification |
| title_full | Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification |
| title_fullStr | Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification |
| title_full_unstemmed | Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification |
| title_short | Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification |
| title_sort | convex polyhedral abstractions specialisation and property based predicate splitting in horn clause verification |
| url | http://arxiv.org/pdf/1412.1154v1 |
| work_keys_str_mv | AT bishoksankafle convexpolyhedralabstractionsspecialisationandpropertybasedpredicatesplittinginhornclauseverification AT johnpgallagher convexpolyhedralabstractionsspecialisationandpropertybasedpredicatesplittinginhornclauseverification |