### Resumé

Originalsprog | Engelsk |
---|---|

Tidsskrift | Electronic Proceedings in Theoretical Computer Science |

Vol/bind | 219 |

Sider (fra-til) | 33-48 |

ISSN | 2075-2180 |

DOI | |

Status | Udgivet - 2016 |

Begivenhed | 3rd Workshop on Horn Clauses for Verification and Synthesis: Workshop affiliated with ETAPS 2016 (The European Joint Conferences on Theory and Practice of Software) - Eindhoven, Eindhoven, Holland Varighed: 3 apr. 2016 → 3 apr. 2016 http://hcvs2016.it.uu.se/ |

### Konference

Konference | 3rd Workshop on Horn Clauses for Verification and Synthesis |
---|---|

Lokation | Eindhoven |

Land | Holland |

By | Eindhoven |

Periode | 03/04/2016 → 03/04/2016 |

Internetadresse |

### Citer dette

*Electronic Proceedings in Theoretical Computer Science*,

*219*, 33-48. https://doi.org/10.4204/EPTCS.219.4

}

*Electronic Proceedings in Theoretical Computer Science*, bind 219, s. 33-48. https://doi.org/10.4204/EPTCS.219.4

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

Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › peer 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 -