Constraint Specialisation in Horn Clause Verification

Bishoksan Kafle, John Patrick Gallagher

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

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 transformation of a given set of clauses and a goal. The effect is to propagate the
constraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; we
use the constraints from the model to compute a specialised version of each clause in the program. The approach is independent of
the abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effective
transformation, both in our own verification tools (convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.
Original languageEnglish
Title of host publicationProceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15
EditorsKenichi Asai, Kostis Sagonas
Number of pages6
Place of PublicationNew York
PublisherAssociation for Computing Machinery
Publication date4 Jan 2015
Pages85-90
ISBN (Print)978-1-4503-3297-2
DOIs
Publication statusPublished - 4 Jan 2015
EventPEPM 2015 - Tata Institute of Fundamental Research, Mumbai, India
Duration: 13 Jan 201514 Jan 2015
http://popl.mpi-sws.org/2015/

Conference

ConferencePEPM 2015
LocationTata Institute of Fundamental Research
CountryIndia
CityMumbai
Period13/01/201514/01/2015
OtherIn cooperation with: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Internet address

Bibliographical note

@inproceedings{DBLP:conf/pepm/KafleG15,
author = {Bishoksan Kafle and
John P. Gallagher},
title = {Constraint Specialisation in Horn Clause Verification},
booktitle = {Proceedings of the 2015 Workshop on Partial Evaluation and Program
Manipulation, PEPM, Mumbai, India, January 15-17, 2015},
pages = {85--90},
year = {2015},
crossref = {DBLP:conf/pepm/2015},
url = {http://doi.acm.org/10.1145/2678015.2682544},
doi = {10.1145/2678015.2682544},
timestamp = {Sun, 04 Jan 2015 11:56:22 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/KafleG15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pepm/2015,
editor = {Kenichi Asai and
Kostis Sagonas},
title = {Proceedings of the 2015 Workshop on Partial Evaluation and Program
Manipulation, PEPM, Mumbai, India, January 15-17, 2015},
publisher = {{ACM}},
year = {2015},
url = {http://dl.acm.org/citation.cfm?id=2678015},
isbn = {978-1-4503-3297-2},
timestamp = {Sun, 04 Jan 2015 11:54:44 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/2015},
bibsource = {dblp computer science bibliography, http://dblp.org}
}

Keywords

  • constraint specialisation
  • query-answer transformation
  • Horn clauses
  • abstract interpretation

Cite this

Kafle, B., & Gallagher, J. P. (2015). Constraint Specialisation in Horn Clause Verification. In K. Asai, & K. Sagonas (Eds.), Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15 (pp. 85-90). New York: Association for Computing Machinery. https://doi.org/10.1145/2678015.2682544
Kafle, Bishoksan ; Gallagher, John Patrick. / Constraint Specialisation in Horn Clause Verification. Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15. editor / Kenichi Asai ; Kostis Sagonas. New York : Association for Computing Machinery, 2015. pp. 85-90
@inproceedings{8d9653154a2b4879827806206aff6af2,
title = "Constraint Specialisation in Horn Clause Verification",
abstract = "We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstractinterpretation to compute a model of a query-answer transformation of a given set of clauses and a goal. The effect is to propagate theconstraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; weuse the constraints from the model to compute a specialised version of each clause in the program. The approach is independent ofthe abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effectivetransformation, both in our own verification tools (convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.",
keywords = "constraint specialisation, query-answer transformation, Horn clauses, abstract interpretation",
author = "Bishoksan Kafle and Gallagher, {John Patrick}",
note = "@inproceedings{DBLP:conf/pepm/KafleG15, author = {Bishoksan Kafle and John P. Gallagher}, title = {Constraint Specialisation in Horn Clause Verification}, booktitle = {Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015}, pages = {85--90}, year = {2015}, crossref = {DBLP:conf/pepm/2015}, url = {http://doi.acm.org/10.1145/2678015.2682544}, doi = {10.1145/2678015.2682544}, timestamp = {Sun, 04 Jan 2015 11:56:22 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/KafleG15}, bibsource = {dblp computer science bibliography, http://dblp.org} } @proceedings{DBLP:conf/pepm/2015, editor = {Kenichi Asai and Kostis Sagonas}, title = {Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015}, publisher = {{ACM}}, year = {2015}, url = {http://dl.acm.org/citation.cfm?id=2678015}, isbn = {978-1-4503-3297-2}, timestamp = {Sun, 04 Jan 2015 11:54:44 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/2015}, bibsource = {dblp computer science bibliography, http://dblp.org} }",
year = "2015",
month = "1",
day = "4",
doi = "10.1145/2678015.2682544",
language = "English",
isbn = "978-1-4503-3297-2",
pages = "85--90",
editor = "Kenichi Asai and Kostis Sagonas",
booktitle = "Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15",
publisher = "Association for Computing Machinery",

}

Kafle, B & Gallagher, JP 2015, Constraint Specialisation in Horn Clause Verification. in K Asai & K Sagonas (eds), Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15. Association for Computing Machinery, New York, pp. 85-90, PEPM 2015, Mumbai, India, 13/01/2015. https://doi.org/10.1145/2678015.2682544

Constraint Specialisation in Horn Clause Verification. / Kafle, Bishoksan; Gallagher, John Patrick.

Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15. ed. / Kenichi Asai; Kostis Sagonas. New York : Association for Computing Machinery, 2015. p. 85-90.

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Constraint Specialisation in Horn Clause Verification

AU - Kafle, Bishoksan

AU - Gallagher, John Patrick

N1 - @inproceedings{DBLP:conf/pepm/KafleG15, author = {Bishoksan Kafle and John P. Gallagher}, title = {Constraint Specialisation in Horn Clause Verification}, booktitle = {Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015}, pages = {85--90}, year = {2015}, crossref = {DBLP:conf/pepm/2015}, url = {http://doi.acm.org/10.1145/2678015.2682544}, doi = {10.1145/2678015.2682544}, timestamp = {Sun, 04 Jan 2015 11:56:22 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/KafleG15}, bibsource = {dblp computer science bibliography, http://dblp.org} } @proceedings{DBLP:conf/pepm/2015, editor = {Kenichi Asai and Kostis Sagonas}, title = {Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015}, publisher = {{ACM}}, year = {2015}, url = {http://dl.acm.org/citation.cfm?id=2678015}, isbn = {978-1-4503-3297-2}, timestamp = {Sun, 04 Jan 2015 11:54:44 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/2015}, bibsource = {dblp computer science bibliography, http://dblp.org} }

PY - 2015/1/4

Y1 - 2015/1/4

N2 - We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstractinterpretation to compute a model of a query-answer transformation of a given set of clauses and a goal. The effect is to propagate theconstraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; weuse the constraints from the model to compute a specialised version of each clause in the program. The approach is independent ofthe abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effectivetransformation, both in our own verification tools (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 abstractinterpretation to compute a model of a query-answer transformation of a given set of clauses and a goal. The effect is to propagate theconstraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; weuse the constraints from the model to compute a specialised version of each clause in the program. The approach is independent ofthe abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effectivetransformation, both in our own verification tools (convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.

KW - constraint specialisation

KW - query-answer transformation

KW - Horn clauses

KW - abstract interpretation

U2 - 10.1145/2678015.2682544

DO - 10.1145/2678015.2682544

M3 - Article in proceedings

SN - 978-1-4503-3297-2

SP - 85

EP - 90

BT - Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15

A2 - Asai, Kenichi

A2 - Sagonas, Kostis

PB - Association for Computing Machinery

CY - New York

ER -

Kafle B, Gallagher JP. Constraint Specialisation in Horn Clause Verification. In Asai K, Sagonas K, editors, Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15. New York: Association for Computing Machinery. 2015. p. 85-90 https://doi.org/10.1145/2678015.2682544