Generalised interpolation by solving recursion free-horn clauses Conference Paper


Author(s): Gupta, Ashutosh K; Popeea, Corneliu; Rybalchenko, Andrey
Title: Generalised interpolation by solving recursion free-horn clauses
Title Series: EPTCS
Affiliation IST Austria
Abstract: In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools.
Keywords: verification; software verification; Problem solving; Interpolation; Application programs; Logic programming; Horn clause; Interpolation problems; Recursions; Verification tools
Conference Title: HCVS: Horn Clauses for Verification and Synthesis
Volume: 169
Conference Dates: July 17 2014
Conference Location: Vienna, Austria
ISBN: 20752180
Publisher: Open Publishing  
Date Published: 2014-12-02
Start Page: 31
End Page: 38
URL:
DOI: 10.4204/EPTCS.169.5
Open access: no
IST Austria Authors
  1. Ashutosh Gupta
    16 Gupta
Related IST Austria Work