Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets

TL;DR

This paper introduces a novel class of nonlinear semialgebraic Craig interpolants for separating disjoint semialgebraic sets, extending polynomial interpolants, with efficient semidefinite programming solutions demonstrated through examples.

Contribution

It proves the existence of semialgebraic interpolants that generalize polynomial ones and provides sum-of-squares characterizations for efficient synthesis.

Findings

Semialgebraic interpolants generalize polynomial interpolants.

Efficient semidefinite programming methods are applicable.

The approach is effective and scalable, demonstrated by examples.

Abstract

Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the cornerstone of these techniques. In this paper, we investigate nonlinear Craig interpolant synthesis for two polynomial formulas of the general form, essentially corresponding to the underlying mathematical problem to separate two disjoint semialgebraic sets. By combining the homogenization approach with existing techniques, we prove the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants. These semialgebraic interpolants subsume polynomial interpolants as a special case. To the best of our knowledge, this is the first existence result of this kind. Furthermore, we provide complete sum-of-squares characterizations for both polynomial and semialgebraic interpolants, which can be efficiently solved as semidefinite programs. Examples are provided to demonstrate the effectiveness and efficiency of our approach.