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 |
| _version_ | 1819019879159693312 |
|---|---|
| author | Ashutosh Gupta Corneliu Popeea Andrey Rybalchenko |
| author_facet | Ashutosh Gupta Corneliu Popeea Andrey Rybalchenko |
| author_sort | Ashutosh Gupta |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-21T03:42:19Z |
| format | Article |
| id | doaj.art-b9f5d0cb9cd14d4188a5dd6024065b81 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-21T03:42:19Z |
| publishDate | 2014-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-b9f5d0cb9cd14d4188a5dd6024065b812022-12-21T19:17:11ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-12-01169Proc. HCVS 2014313810.4204/EPTCS.169.5:6Generalised Interpolation by Solving Recursion-Free Horn ClausesAshutosh GuptaCorneliu PopeeaAndrey RybalchenkoIn 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.http://arxiv.org/pdf/1303.7378v2 |
| spellingShingle | Ashutosh Gupta Corneliu Popeea Andrey Rybalchenko Generalised Interpolation by Solving Recursion-Free Horn Clauses Electronic Proceedings in Theoretical Computer Science |
| title | Generalised Interpolation by Solving Recursion-Free Horn Clauses |
| title_full | Generalised Interpolation by Solving Recursion-Free Horn Clauses |
| title_fullStr | Generalised Interpolation by Solving Recursion-Free Horn Clauses |
| title_full_unstemmed | Generalised Interpolation by Solving Recursion-Free Horn Clauses |
| title_short | Generalised Interpolation by Solving Recursion-Free Horn Clauses |
| title_sort | generalised interpolation by solving recursion free horn clauses |
| url | http://arxiv.org/pdf/1303.7378v2 |
| work_keys_str_mv | AT ashutoshgupta generalisedinterpolationbysolvingrecursionfreehornclauses AT corneliupopeea generalisedinterpolationbysolvingrecursionfreehornclauses AT andreyrybalchenko generalisedinterpolationbysolvingrecursionfreehornclauses |