The Relationship between Craig Interpolation and Recursion-Free Horn Clauses

TL;DR

This paper explores the connection between Craig interpolation and recursion-free Horn clauses, showing their equivalence and discussing methods for solving such constraints to aid software verification.

Contribution

It provides a comprehensive survey of Craig interpolation forms and demonstrates their correspondence to recursion-free Horn constraints, highlighting their relevance in verification.

Findings

All Craig interpolation forms correspond to natural fragments of recursion-free Horn constraints

Techniques for solving systems of recursion-free Horn constraints are discussed

The survey clarifies the role of Craig interpolation in verification processes

Abstract

Despite decades of research, there are still a number of concepts commonly found in software programs that are considered challenging for verification: among others, such concepts include concurrency, and the compositional analysis of programs with procedures. As a promising direction to overcome such difficulties, recently the use of Horn constraints as intermediate representation of software programs has been proposed. Horn constraints are related to Craig interpolation, which is one of the main techniques used to construct and refine abstractions in verification, and to synthesise inductive loop invariants. We give a survey of the different forms of Craig interpolation found in literature, and show that all of them correspond to natural fragments of (recursion-free) Horn constraints. We also discuss techniques for solving systems of recursion-free Horn constraints.