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

Programmering, logik og intelligente systemer

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

13 Citationer (Scopus)

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

Originalsprog	Engelsk
Titel	Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15
Redaktører	Kenichi Asai, Kostis Sagonas
Antal sider	6
Udgivelsessted	New York
Forlag	Association for Computing Machinery
Publikationsdato	4 jan. 2015
Sider	85-90
ISBN (Trykt)	978-1-4503-3297-2
DOI	https://doi.org/10.1145/2678015.2682544
Status	Udgivet - 4 jan. 2015
Begivenhed	PEPM 2015 - Tata Institute of Fundamental Research, Mumbai, Indien Varighed: 13 jan. 2015 → 14 jan. 2015 http://popl.mpi-sws.org/2015/

Konference

Konference	PEPM 2015
Lokation	Tata Institute of Fundamental Research
Land/Område	Indien
By	Mumbai
Periode	13/01/2015 → 14/01/2015
Andet	In cooperation with: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Internetadresse	http://popl.mpi-sws.org/2015/

Link til dokument

10.1145/2678015.2682544

pepm19s-kafle-gallagher-mainAccepteret manuskript, 327 KB

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

Citer dette

@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} }; 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. red. / Kenichi Asai; Kostis Sagonas. New York: Association for Computing Machinery, 2015. s. 85-90.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › 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 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

T2 - PEPM 2015

Y2 - 13 January 2015 through 14 January 2015

ER -

Constraint Specialisation in Horn Clause Verification

Abstract

Konference

Link til dokument

Projekter

ENTRA: Whole-Systems Energy Transparency

NUSA: Numeric and Symbolic Abstractions for Software Model Checking

Citer dette