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

Bishoksan Kafle, John Patrick Gallagher, Pierre Ganty

Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

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.
OriginalsprogEngelsk
TidsskriftElectronic Proceedings in Theoretical Computer Science
Vol/bind219
Sider (fra-til)33-48
Antal sider16
ISSN2075-2180
DOI
StatusUdgivet - 14 jul. 2016
Begivenhed3rd 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. 20163 apr. 2016
http://hcvs2016.it.uu.se/

Konference

Konference3rd Workshop on Horn Clauses for Verification and Synthesis
LokationEindhoven
Land/OmrådeHolland
ByEindhoven
Periode03/04/201603/04/2016
Internetadresse

Citer dette