Interpolant tree automata and their application in Horn clause verification

Bishoksan Kafle, John Patrick Gallagher

Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

Resumé

This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn clause verification. These techniques have been previously applied separately, but are combined in a new way in this paper. The role of an interpolant tree automaton is to provide a generalisation of a spurious counterexample during refinement, capturing a possibly infinite set of spurious counterexample traces. In our approach these traces are then eliminated using a transformation of the Horn clauses. We compare this approach with two other methods; one of them uses interpolant tree automata in an algorithm for trace abstraction and refinement, while the other uses abstract interpretation over the domain of convex polyhedra without the generalisation step. Evaluation of the results of experiments on a number of Horn clause verification problems indicates that the combination of interpolant tree automaton with abstract interpretation gives some increase in the power of the verification tool, while sometimes incurring a performance overhead.

Workshop

WorkshopFourth International Workshop on Verification and Program Transformation
LandHolland
ByEindhoven
Periode02/04/201602/04/2016
Internetadresse

Emneord

    Citer dette

    @inproceedings{6f63c991300c490785df9127eb69f6c0,
    title = "Interpolant tree automata and their application in Horn clause verification",
    abstract = "This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn clause verification. These techniques have been previously applied separately, but are combined in a new way in this paper. The role of an interpolant tree automaton is to provide a generalisation of a spurious counterexample during refinement, capturing a possibly infinite set of spurious counterexample traces. In our approach these traces are then eliminated using a transformation of the Horn clauses. We compare this approach with two other methods; one of them uses interpolant tree automata in an algorithm for trace abstraction and refinement, while the other uses abstract interpretation over the domain of convex polyhedra without the generalisation step. Evaluation of the results of experiments on a number of Horn clause verification problems indicates that the combination of interpolant tree automaton with abstract interpretation gives some increase in the power of the verification tool, while sometimes incurring a performance overhead.",
    keywords = "Program analysis, Program verification, Horn clauses, Interpolation",
    author = "Bishoksan Kafle and Gallagher, {John Patrick}",
    year = "2016",
    doi = "10.4204/EPTCS.216.6",
    language = "English",
    volume = "216",
    pages = "104--117",
    journal = "Electronic Proceedings in Theoretical Computer Science",
    issn = "2075-2180",
    publisher = "Open Publishing Association",

    }

    Interpolant tree automata and their application in Horn clause verification. / Kafle, Bishoksan; Gallagher, John Patrick.

    I: Electronic Proceedings in Theoretical Computer Science, Bind 216, 2016, s. 104-117.

    Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

    TY - GEN

    T1 - Interpolant tree automata and their application in Horn clause verification

    AU - Kafle, Bishoksan

    AU - Gallagher, John Patrick

    PY - 2016

    Y1 - 2016

    N2 - This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn clause verification. These techniques have been previously applied separately, but are combined in a new way in this paper. The role of an interpolant tree automaton is to provide a generalisation of a spurious counterexample during refinement, capturing a possibly infinite set of spurious counterexample traces. In our approach these traces are then eliminated using a transformation of the Horn clauses. We compare this approach with two other methods; one of them uses interpolant tree automata in an algorithm for trace abstraction and refinement, while the other uses abstract interpretation over the domain of convex polyhedra without the generalisation step. Evaluation of the results of experiments on a number of Horn clause verification problems indicates that the combination of interpolant tree automaton with abstract interpretation gives some increase in the power of the verification tool, while sometimes incurring a performance overhead.

    AB - This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn clause verification. These techniques have been previously applied separately, but are combined in a new way in this paper. The role of an interpolant tree automaton is to provide a generalisation of a spurious counterexample during refinement, capturing a possibly infinite set of spurious counterexample traces. In our approach these traces are then eliminated using a transformation of the Horn clauses. We compare this approach with two other methods; one of them uses interpolant tree automata in an algorithm for trace abstraction and refinement, while the other uses abstract interpretation over the domain of convex polyhedra without the generalisation step. Evaluation of the results of experiments on a number of Horn clause verification problems indicates that the combination of interpolant tree automaton with abstract interpretation gives some increase in the power of the verification tool, while sometimes incurring a performance overhead.

    KW - Program analysis

    KW - Program verification

    KW - Horn clauses

    KW - Interpolation

    U2 - 10.4204/EPTCS.216.6

    DO - 10.4204/EPTCS.216.6

    M3 - Conference article

    VL - 216

    SP - 104

    EP - 117

    JO - Electronic Proceedings in Theoretical Computer Science

    JF - Electronic Proceedings in Theoretical Computer Science

    SN - 2075-2180

    ER -