Projects per year
Abstract
In this paper we show that checking satisfiability of a set of nonlinear Horn clauses (also called a nonlinear 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 nonlinear 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.
Original language  English 

Journal  Electronic Proceedings in Theoretical Computer Science 
Volume  219 
Pages (fromto)  3348 
ISSN  20752180 
DOIs  
Publication status  Published  2016 
Event  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, Netherlands Duration: 3 Apr 2016 → 3 Apr 2016 http://hcvs2016.it.uu.se/ 
Conference
Conference  3rd Workshop on Horn Clauses for Verification and Synthesis 

Location  Eindhoven 
Country/Territory  Netherlands 
City  Eindhoven 
Period  03/04/2016 → 03/04/2016 
Internet address 
Keywords
 Program analysis
 Program verification
 Horn clauses
Projects
 2 Finished


ENTRA: WholeSystems Energy Transparency
Gallagher, J. P., Rosendahl, M., Rhiger, M., Strand, D. L. & Bohr, N.
01/10/2012 → 30/09/2015
Project: Research