# Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)

arXiv: https://arxiv.org/abs/1301.4973 · HTML: https://mlsanity.com/paper/1301.4973/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Jan 2013.

## Built on by (most cited first, 2 of 2)

- [The Horn Non-Clausal Class and its Polynomiality](https://mlsanity.com/paper/2108.13744/) (2021)
- [Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)](https://mlsanity.com/paper/2206.06986/) (2022)

## Abstract (arXiv)

One of the main challenges in software verification is efficient and precise compositional analysis of programs with procedures and loops. Interpolation methods remain one of the most promising techniques for such verification, 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 verification algorithms that use disjunctive interpolants and evaluate them on benchmarks expressed as Horn clauses over the theory of integer linear arithmetic.