Generalised Interpolation by Solving Recursion-Free Horn Clauses

TL;DR

This paper introduces InterHorn, a solver for recursion-free Horn clauses, specifically designed for various interpolation problems in software verification, aiming to unify and streamline verification processes.

Contribution

The paper presents a new solver, InterHorn, capable of handling diverse interpolation problems directly through Horn clause representations, promoting a common verification interface.

Findings

InterHorn effectively solves multiple types of interpolation problems.

It enables a unified approach for diverse verification tools.

The solver improves efficiency in software verification workflows.

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.