Solving non-linear Horn clauses using a linear Horn clause solver

Bishoksan Kafle, John Patrick Gallagher, Pierre Ganty

Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

Resumé

In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Horn clauses to a sequence of sets of clauses with successively increasing dimension bound. The approach is then further developed by using a solution of clauses of lower dimension to (partially) linearise clauses of higher dimension. We constructed a prototype implementation of this approach and performed some experiments on a set of verification problems, which shows some promise.

Konference

Konference3rd Workshop on Horn Clauses for Verification and Synthesis
LokationEindhoven
LandHolland
Periode03/04/201603/04/2016
Internetadresse

Emneord

    Citer dette

    @inproceedings{df23ea206b204aa5a3495849141a5139,
    title = "Solving non-linear Horn clauses using a linear Horn clause solver",
    abstract = "In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Horn clauses to a sequence of sets of clauses with successively increasing dimension bound. The approach is then further developed by using a solution of clauses of lower dimension to (partially) linearise clauses of higher dimension. We constructed a prototype implementation of this approach and performed some experiments on a set of verification problems, which shows some promise.",
    keywords = "Program analysis, Program verification, Horn clauses",
    author = "Bishoksan Kafle and Gallagher, {John Patrick} and Pierre Ganty",
    year = "2016",
    doi = "10.4204/EPTCS.219.4",
    language = "English",
    volume = "219",
    pages = "33--48",
    journal = "Electronic Proceedings in Theoretical Computer Science",
    issn = "2075-2180",
    publisher = "Open Publishing Association",

    }

    Solving non-linear Horn clauses using a linear Horn clause solver. / Kafle, Bishoksan; Gallagher, John Patrick; Ganty, Pierre.

    I: Electronic Proceedings in Theoretical Computer Science, Bind 219, 2016, s. 33-48.

    Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

    TY - GEN

    T1 - Solving non-linear Horn clauses using a linear Horn clause solver

    AU - Kafle, Bishoksan

    AU - Gallagher, John Patrick

    AU - Ganty, Pierre

    PY - 2016

    Y1 - 2016

    N2 - In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Horn clauses to a sequence of sets of clauses with successively increasing dimension bound. The approach is then further developed by using a solution of clauses of lower dimension to (partially) linearise clauses of higher dimension. We constructed a prototype implementation of this approach and performed some experiments on a set of verification problems, which shows some promise.

    AB - In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Horn clauses to a sequence of sets of clauses with successively increasing dimension bound. The approach is then further developed by using a solution of clauses of lower dimension to (partially) linearise clauses of higher dimension. We constructed a prototype implementation of this approach and performed some experiments on a set of verification problems, which shows some promise.

    KW - Program analysis

    KW - Program verification

    KW - Horn clauses

    U2 - 10.4204/EPTCS.219.4

    DO - 10.4204/EPTCS.219.4

    M3 - Conference article

    VL - 219

    SP - 33

    EP - 48

    JO - Electronic Proceedings in Theoretical Computer Science

    JF - Electronic Proceedings in Theoretical Computer Science

    SN - 2075-2180

    ER -