Interpolation Properties and SAT-based Model Checking

TL;DR

This paper introduces a unified framework for analyzing the properties of Craig interpolation in SAT-based model checking, enabling systematic comparison and understanding of the necessary conditions for effective verification.

Contribution

It presents a general framework that encompasses common interpolation collectives, facilitating systematic study and comparison across different verification systems.

Findings

Unified framework for interpolation collectives

Systematic analysis of constraints on propositional interpolation

Comparison of interpolation systems in verification contexts

Abstract

Craig interpolation is a widespread method in verification, with important applications such as Predicate Abstraction, CounterExample Guided Abstraction Refinement and Lazy Abstraction With Interpolants. Most state-of-the-art model checking techniques based on interpolation require collections of interpolants to satisfy particular properties, to which we refer as "collectives"; they do not hold in general for all interpolation systems and have to be established for each particular system and verification environment. Nevertheless, no systematic approach exists that correlates the individual interpolation systems and compares the necessary collectives. This paper proposes a uniform framework, which encompasses (and generalizes) the most common collectives exploited in verification. We use it for a systematic study of the collectives and of the constraints they pose on propositional interpolation systems used in SAT-based model checking.