--- res: bibo_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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Ashutosh foaf_name: Gupta, Ashutosh foaf_surname: Gupta foaf_workInfoHomepage: http://www.librecat.org/personId=335E5684-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Corneliu foaf_name: Popeea, Corneliu foaf_surname: Popeea - foaf_Person: foaf_givenName: Andrey foaf_name: Rybalchenko, Andrey foaf_surname: Rybalchenko bibo_doi: 10.4204/EPTCS.169.5 bibo_volume: 169 dct_date: 2014^xs_gYear dct_language: eng dct_publisher: Open Publishing@ dct_title: Generalised interpolation by solving recursion free-horn clauses@ ...