Constraint specialisation in Horn clause verification

Bishoksan Kafle, John Patrick Gallagher

Publikation: Bidrag til tidsskriftTidsskriftartikel

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 transformed version of a given set of clauses and a goal. The constraints from the model are then used to compute a specialised version of each clause. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. The specialisation procedure can be repeated to yield further specialisation. The approach is independent of the abstract domain and the constraint theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (based on a convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.
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 transformed version of a given set of clauses and a goal. The constraints from the model are then used to compute a specialised version of each clause. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. The specialisation procedure can be repeated to yield further specialisation. The approach is independent of the abstract domain and the constraint theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (based on a convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.
SprogEngelsk
TidsskriftScience of Computer Programming
Vol/bind137
Sider125-140
ISSN0167-6423
DOI
StatusUdgivet - 1 apr. 2017

Emneord

    Citer dette

    @article{d378e486d23a48a5be57f272df6c2226,
    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 transformed version of a given set of clauses and a goal. The constraints from the model are then used to compute a specialised version of each clause. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. The specialisation procedure can be repeated to yield further specialisation. The approach is independent of the abstract domain and the constraint theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (based on a convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.",
    keywords = "Constraint specialisation, Query–answer transformation, Program verification, program analysis, Abstract Interpretation",
    author = "Bishoksan Kafle and Gallagher, {John Patrick}",
    year = "2017",
    month = "4",
    day = "1",
    doi = "10.1016/j.scico.2017.01.002",
    language = "English",
    volume = "137",
    pages = "125--140",
    journal = "Science of Computer Programming",
    issn = "0167-6423",
    publisher = "Elsevier BV",

    }

    Constraint specialisation in Horn clause verification. / Kafle, Bishoksan; Gallagher, John Patrick.

    I: Science of Computer Programming, Bind 137, 01.04.2017, s. 125-140.

    Publikation: Bidrag til tidsskriftTidsskriftartikel

    TY - JOUR

    T1 - Constraint specialisation in Horn clause verification

    AU - Kafle,Bishoksan

    AU - Gallagher,John Patrick

    PY - 2017/4/1

    Y1 - 2017/4/1

    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 transformed version of a given set of clauses and a goal. The constraints from the model are then used to compute a specialised version of each clause. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. The specialisation procedure can be repeated to yield further specialisation. The approach is independent of the abstract domain and the constraint theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (based on a 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 transformed version of a given set of clauses and a goal. The constraints from the model are then used to compute a specialised version of each clause. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. The specialisation procedure can be repeated to yield further specialisation. The approach is independent of the abstract domain and the constraint theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (based on a convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.

    KW - Constraint specialisation

    KW - Query–answer transformation

    KW - Program verification

    KW - program analysis

    KW - Abstract Interpretation

    U2 - 10.1016/j.scico.2017.01.002

    DO - 10.1016/j.scico.2017.01.002

    M3 - Journal article

    VL - 137

    SP - 125

    EP - 140

    JO - Science of Computer Programming

    T2 - Science of Computer Programming

    JF - Science of Computer Programming

    SN - 0167-6423

    ER -