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.

翻译：Craig插值在程序验证中被用于自动化关键任务，如循环不变式的推断和程序抽象的计算。本章涵盖了近年来在此背景下发展出的一些最重要技术，重点关注两个方面：基于验证所用理论和数据类型的Craig插值推导方法，以及应用插值技术的验证算法基础设计。