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