Generalised Interpolation by Solving Recursion-Free Horn Clauses
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1303.7378v2 |
| Summary: | 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. |
|---|---|
| ISSN: | 2075-2180 |