Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Craig Interpolation in Program Verification

Philipp Rümmer

TL;DR

This chapter surveys Craig interpolation as a core technique in program verification, focusing on how interpolants can be computed modulo theories such as linear real and integer arithmetic and how they drive verification algorithms. It details foundational definitions (SMT, theories, and theory-based interpolation), extended forms (sequence and tree interpolants), and practical interpolation methods (proof-based, graph-based, and reductions). The chapter then integrates these techniques with major verification paradigms: BMC, IMC, CEGAR with existential/predicate abstractions, and CHCs for recursive programs, illustrating how interpolants yield invariants and abstractions. The discussion highlights completeness results, algorithmic trade-offs, and extensions to combine multiple theories, aiming to guide the design of effective interpolation-based verification tools with practical applicability across hardware and software analysis.

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.

Craig Interpolation in Program Verification

TL;DR

This chapter surveys Craig interpolation as a core technique in program verification, focusing on how interpolants can be computed modulo theories such as linear real and integer arithmetic and how they drive verification algorithms. It details foundational definitions (SMT, theories, and theory-based interpolation), extended forms (sequence and tree interpolants), and practical interpolation methods (proof-based, graph-based, and reductions). The chapter then integrates these techniques with major verification paradigms: BMC, IMC, CEGAR with existential/predicate abstractions, and CHCs for recursive programs, illustrating how interpolants yield invariants and abstractions. The discussion highlights completeness results, algorithmic trade-offs, and extensions to combine multiple theories, aiming to guide the design of effective interpolation-based verification tools with practical applicability across hardware and software analysis.

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.
Paper Structure (30 sections, 5 theorems, 27 equations, 8 figures, 1 table)

This paper contains 30 sections, 5 theorems, 27 equations, 8 figures, 1 table.

Table of Contents

  1. Introduction
  2. Informal Overview: Invariant Inference using Craig Interpolation
  3. Organization of the Chapter
  4. Satisfiability and Interpolation Modulo Theories
  5. Basic Definitions
  6. First-Order Logic and Theories
  7. Craig Interpolation Modulo Theories
  8. Extended Forms of Craig Interpolation
  9. Interpolation Modulo Linear Arithmetic
  10. Linear Real Arithmetic (LRA)
  11. Beyond Conjunctions of Non-strict Inequalities
  12. Linear Integer Arithmetic (LIA)
  13. Further Interpolation Approaches
  14. Proof-Based Interpolation
  15. Graph-Based Interpolation
  16. ...and 15 more sections

Key Result

Theorem 5

Suppose that $T$ is a theory and $A \wedge B$ a sentence that is $T$-unsatisfiable. Then there is a $T$-separator for $A \wedge B$; more precisely, there are $T$-separators $I_1, I_2$ such that:

Figures (8)

  • Figure 1: Fibonacci program and the conditions for inductive loop invariants.
  • Figure 2: Unwinding two iterations of the loop in the Fibonacci program.
  • Figure 3: Intermediate assertions.
  • Figure 4: Proof of unsatisfiability for $\Gamma = \{0 \leq y - 1, 0 \leq z - x - 2y - 2, 0 \leq x, 0 \leq -z + 2\}$ in Example \ref{['ex:lra-1']}.
  • Figure 5: Interpolating version of the proof in Fig. \ref{['fig:lra-example-proof']}. We use the abbreviation $\Gamma^I = (A, B) = (\{0 \leq y - 1, 0 \leq z - x - 2y - 2\}, \{0 \leq x, 0 \leq -z + 2\})$.
  • ...and 3 more figures

Theorems & Definitions (20)

  • Definition 1: Theory
  • Definition 2: Craig interpolant modulo theory
  • Example 3
  • Definition 4: Separator, reverse Craig interpolant
  • Theorem 5: Existence of $T$-separators DBLP:conf/cade/KovacsV09
  • Example 6
  • Definition 7: General quantifier-free interpolation DBLP:journals/tocl/BruttomessoGR14
  • Definition 8: Plain quantifier-free interpolation DBLP:journals/tocl/BruttomessoGR14
  • Example 9
  • Definition 10: Sequence interpolant DBLP:conf/popl/HenzingerJMM04DBLP:conf/cav/McMillan06
  • ...and 10 more