Craig Interpolation in Program Verification

TL;DR

This paper reviews the use of Craig interpolation in program verification, focusing on techniques for deriving interpolants across various theories and their role in verification algorithms.

Contribution

It provides a comprehensive overview of recent techniques for deriving Craig interpolants and their application in automating verification tasks.

Findings

Enhanced methods for deriving interpolants in different theories

Integration of interpolation techniques into verification algorithms

Improved automation of loop invariant inference

Abstract

Craig interpolation is used in program verification for automating key tasks such as the inference of loop invariants and the computation of program abstractions. This chapter covers some of the most important techniques that have been developed in this context over the last years, focusing on two aspects: the derivation of Craig interpolants modulo the theories and data types used in verification and the basic design of verification algorithms applying interpolation.