Generalised Interpolation By Solving Recursion-Free Horn Clauses
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE(2014)
摘要
In this paper we present INTERHORN, a solver for recursion- freeHorn 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要