Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

Bishoksan Kafle, John Patrick Gallagher

Publikation: Bidrag til tidsskriftTidsskriftartikel

Resumé

In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision. We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state-of-the-art Horn clause verification tools.
In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision. We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state-of-the-art Horn clause verification tools.
SprogEngelsk
TidsskriftComputer Languages, Systems and Structures
Vol/bind47
Udgave nummerPart 1
Sider2-18
ISSN1477-8424
DOI
StatusUdgivet - jan. 2017

Emneord

    Citer dette

    @article{7e9efb5ce9f3412694d25b8a14d5f12c,
    title = "Horn clause verification with convex polyhedral abstraction and tree automata-based refinement",
    abstract = "In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision. We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state-of-the-art Horn clause verification tools.",
    keywords = "static analysis, Program verification, tree automata",
    author = "Bishoksan Kafle and Gallagher, {John Patrick}",
    year = "2017",
    month = "1",
    doi = "10.1016/j.cl.2015.11.001",
    language = "English",
    volume = "47",
    pages = "2--18",
    journal = "Computer Languages, Systems and Structures",
    issn = "1477-8424",
    publisher = "Pergamon Press",
    number = "Part 1",

    }

    Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. / Kafle, Bishoksan; Gallagher, John Patrick.

    I: Computer Languages, Systems and Structures, Bind 47, Nr. Part 1, 01.2017, s. 2-18.

    Publikation: Bidrag til tidsskriftTidsskriftartikel

    TY - JOUR

    T1 - Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

    AU - Kafle,Bishoksan

    AU - Gallagher,John Patrick

    PY - 2017/1

    Y1 - 2017/1

    N2 - In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision. We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state-of-the-art Horn clause verification tools.

    AB - In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision. We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state-of-the-art Horn clause verification tools.

    KW - static analysis

    KW - Program verification

    KW - tree automata

    U2 - 10.1016/j.cl.2015.11.001

    DO - 10.1016/j.cl.2015.11.001

    M3 - Journal article

    VL - 47

    SP - 2

    EP - 18

    JO - Computer Languages, Systems and Structures

    T2 - Computer Languages, Systems and Structures

    JF - Computer Languages, Systems and Structures

    SN - 1477-8424

    IS - Part 1

    ER -