Interpolant Generation

Introduction to Interpolation

Given two contradictory formulas A and B, a Craig interpolant I is a formula that satisfies the following conditions:

  • I is a logical consequence of A.

  • I and B are contradictory

  • I contains only the variables that are common to A and B.

Craig interpolant is a formula that captures the shared information between A and B, and “explains” why they are contradictory. Craig interpolants have several important applications in model checking

  • Abstraction refinement in verification

  • Approximating the image computation in verification

  • …?

The computation of Craig interpolants is a challenging problem, and various algorithms and techniques have been developed to compute them efficiently. For example, for Boolean formulas, interpolants can be extracted from resolution proofs.

Several approaches exist for computing Craig interpolants:

1. Proof-Based Methods

  • Extract interpolants from resolution proofs

  • Transform proofs generated by SAT solvers

  • Handle theory-specific interpolation

2. Symbol Elimination

  • Eliminate non-shared symbols through quantification

  • Apply quantifier elimination techniques

3. Template-based Approaches

  • Start with parameterized templates

  • Solve constraint systems to find parameters

Interpolant Generation in Arlib

Usage Examples

from arlib import
# TBD

References

  • McMillan, K. L. (2003). “Interpolation and SAT-based Model Checking.” In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD)

  • Henzinger, T. A., Jhala, R., Majumdar, R., & McMillan, K. L. (2004). “Abstractions from proofs.” In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

  • D’Silva, V., Kroening, D., Purandare, M., & Weissenbacher, G. (2010). “Interpolant strength.” In International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI)