Constraint Specialisation in Horn Clause Verification

Bishoksan Kafle, John Patrick Gallagher

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

Resumé

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.
OriginalsprogEngelsk
TitelProceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15
RedaktørerKenichi Asai, Kostis Sagonas
Antal sider6
Udgivelses stedNew York
ForlagAssociation for Computing Machinery
Publikationsdato4 jan. 2015
Sider85-90
ISBN (Trykt)978-1-4503-3297-2
DOI
StatusUdgivet - 4 jan. 2015
BegivenhedPEPM 2015 - Tata Institute of Fundamental Research, Mumbai, Indien
Varighed: 13 jan. 201514 jan. 2015
http://popl.mpi-sws.org/2015/

Konference

KonferencePEPM 2015
LokationTata Institute of Fundamental Research
LandIndien
ByMumbai
Periode13/01/201514/01/2015
AndetIn cooperation with: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Internetadresse

Emneord

    Citer dette

    Kafle, B., & Gallagher, J. P. (2015). Constraint Specialisation in Horn Clause Verification. I K. Asai, & K. Sagonas (red.), Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15 (s. 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. red. / Kenichi Asai ; Kostis Sagonas. New York : Association for Computing Machinery, 2015. s. 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. i K Asai & K Sagonas (red), Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15. Association for Computing Machinery, New York, s. 85-90, Mumbai, Indien, 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. red. / Kenichi Asai; Kostis Sagonas. New York : Association for Computing Machinery, 2015. s. 85-90.

    Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer 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. I Asai K, Sagonas K, red., Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15. New York: Association for Computing Machinery. 2015. s. 85-90 https://doi.org/10.1145/2678015.2682544