Name
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.4204/EPTCS.219.4 | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE |
DocType | Volume | Issue |
Journal | abs/1607.04459 | 219 |
ISSN | Citations | PageRank |
2075-2180 | 2 | 0.36 |
References | Authors | |
8 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| bishoksan kafle | 1 | 39 | 7.88 |
| John P. Gallagher | 2 | 984 | 59.94 |
| Pierre Ganty | 3 | 242 | 20.29 |