Generalised Interpolation by Solving Recursion-Free Horn Clauses

Ashutosh Gupta
Corneliu Popeea
Andrey Rybalchenko

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.

In Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko and Valerio Senni: Proceedings First Workshop on Horn Clauses for Verification and Synthesis (HCVS 2014), Vienna, Austria, 17 July 2014, Electronic Proceedings in Theoretical Computer Science 169, pp. 31–38.
Published: 2nd December 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.169.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org