Projekter pr. år
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.
Originalsprog | Engelsk |
---|---|
Tidsskrift | Electronic Proceedings in Theoretical Computer Science |
Vol/bind | 219 |
Sider (fra-til) | 33-48 |
Antal sider | 16 |
ISSN | 2075-2180 |
DOI | |
Status | Udgivet - 14 jul. 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/Område | Holland |
By | Eindhoven |
Periode | 03/04/2016 → 03/04/2016 |
Internetadresse |
Projekter
- 2 Afsluttet
-
ICT-Energy
Gallagher, J. P. (Projektdeltager), Rosendahl, M. (Projektdeltager) & Bohr, N. (Projektdeltager)
01/10/2013 → 30/09/2016
Projekter: Projekt › Forskning
-
ENTRA: Whole-Systems Energy Transparency
Gallagher, J. P. (Projektdeltager), Rosendahl, M. (Projektdeltager), Rhiger, M. (Projektdeltager), Strand, D. L. (Projektleder) & Bohr, N. (Projektdeltager)
01/10/2012 → 30/09/2015
Projekter: Projekt › Forskning