Constraint Specialisation in Horn Clause Verification

Bishoksan Kafle; John Patrick Gallagher

doi:10.1145/2678015.2682544

Constraint Specialisation in Horn Clause Verification

Bishoksan Kafle
, John Patrick Gallagher

Programming, Logic and Intelligent Systems

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

13 Citations (Scopus)

884 Downloads (Pure)

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 language	English
Title of host publication	Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15
Editors	Kenichi Asai, Kostis Sagonas
Number of pages	6
Place of Publication	New York
Publisher	Association for Computing Machinery
Publication date	4 Jan 2015
Pages	85-90
ISBN (Print)	978-1-4503-3297-2
DOIs	https://doi.org/10.1145/2678015.2682544
Publication status	Published - 4 Jan 2015
Event	PEPM 2015 - Tata Institute of Fundamental Research, Mumbai, India Duration: 13 Jan 2015 → 14 Jan 2015 http://popl.mpi-sws.org/2015/

Conference

Conference	PEPM 2015
Location	Tata Institute of Fundamental Research
Country/Territory	India
City	Mumbai
Period	13/01/2015 → 14/01/2015
Other	In cooperation with: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Internet address	http://popl.mpi-sws.org/2015/

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

Access to Document

10.1145/2678015.2682544

pepm19s-kafle-gallagher-mainAccepted author manuscript, 327 KB

ENTRA: Whole-Systems Energy Transparency
Kafle, B. (Project participant)
FP7
01/10/2012 → 30/09/2015
Project: Research
NUSA: Numeric and Symbolic Abstractions for Software Model Checking
Gallagher, J. P. (Project participant), Rosendahl, M. (Project participant) & Rhiger, M. (Project participant)
01/01/2011 → 31/12/2013
Project: Research

Citation Styles

@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 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.",

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\} \}; PEPM 2015 ; Conference date: 13-01-2015 Through 14-01-2015",

year = "2015",

month = jan,

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",

url = "http://popl.mpi-sws.org/2015/",

}

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 proceeding › Article in proceedings › Research › peer-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 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.

AB - 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.

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

T2 - PEPM 2015

Y2 - 13 January 2015 through 14 January 2015

ER -

Constraint Specialisation in Horn Clause Verification

Abstract

Conference

Bibliographical note

Keywords

Access to Document

Projects

ENTRA: Whole-Systems Energy Transparency

NUSA: Numeric and Symbolic Abstractions for Software Model Checking

Citation Styles