On recursion-free Horn clauses and Craig interpolation

One of the main challenges in software verification is efficient and precise analysis of programs with procedures and loops. Interpolation methods remain among the most promising techniques for such verification. To accommodate the demands of various programming language features, over the past years several extended forms of interpolation have been introduced. We give a precise ontology of such extended interpolation methods, and investigate the relationship between interpolation and fragments of constrained recursion-free Horn clauses. We also introduce a new notion of interpolation, disjunctive interpolation, which solves a more general class of problems in one step compared to previous notions of interpolants, such as tree interpolants or inductive sequences of interpolants. We present algorithms and complexity for construction of interpolants, as well as the corresponding decision problems for recursion-free Horn fragments. Finally, we give an extensive empirical evaluation using a solver for (recursive) Horn problems, in particular comparing the performance of tree interpolation and disjunctive interpolation for constraints modelling software verification tasks.