Generalised Interpolation by Solving Recursion-Free Horn Clauses
Logic in Computer Science
2014-12-04 v2
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.
Cite
@article{arxiv.1303.7378,
title = {Generalised Interpolation by Solving Recursion-Free Horn Clauses},
author = {Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko},
journal= {arXiv preprint arXiv:1303.7378},
year = {2014}
}
Comments
In Proceedings HCVS 2014, arXiv:1412.0825