Disjunctive interpolants for Horn-clause verification

Abstract. One of the main challenges in software verification is efficient and precise compositional analysis of programs with procedures and loops. Interpo-lation methods remains one of the most promising techniques for such verifica-tion, and are closely related to solving Horn clause constraints. We introduce a new notion of interpolation, disjunctive interpolation, which solve 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 disjunctive interpolants, as well as their use within an abstraction-refinement loop. We have implemented Horn clause verifi-cation algorithms that use disjunctive interpolants and evaluate them on bench-marks expressed as Horn clauses over the theory of integer linear arithmetic.