Nonlinear Craig Interpolant Generation

TL;DR

This paper introduces a method for generating nonlinear Craig interpolants for polynomial formulas using semi-definite programming, enhancing the scalability of formal verification techniques involving nonlinear theories.

Contribution

It proves the existence of polynomial interpolants for certain nonlinear formulas and reduces their synthesis to semi-definite programming, with a verification method to ensure soundness.

Findings

Existence of polynomial interpolants for specific nonlinear formulas.

Reduction of interpolant synthesis to semi-definite programming.

A verification approach to ensure the soundness of the interpolants.

Abstract

Interpolation-based techniques have become popularized in recent years because of their inherently modular and local reasoning, which can scale up existing formal verification techniques like theorem proving, model-checking, abstraction interpretation, and so on, while the scalability is the bottleneck of these techniques. Craig interpolant generation plays a central role in interpolation-based techniques, and therefore has drawn increasing attentions. In the literature, there are various works done on how to automatically synthesize interpolants for decidable fragments of first-order logic, linear arithmetic, array logic, equality logic with uninterpreted functions (EUF), etc., and their combinations. But Craig interpolant generation for non-linear theory and its combination with the aforementioned theories are still in infancy, although some attempts have been done. In this paper, we first prove that a polynomial interpolant of the form $h(\mathbf{x})>0$ exists for two mutually contradictory polynomial formulas $\phi(\mathbf{x},\mathbf{y})$ and $\psi(\mathbf{x},\mathbf{z})$, with the form $f_1\ge0\wedge\cdots\wedge f_n\ge0$, where $f_i$ are polynomials in $\mathbf{x},\mathbf{y}$ or $\mathbf{x},\mathbf{z}$, and the quadratic module generated by $f_i$ is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem (${\rm SDP}$). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in ${\rm SDP}$ solving. Finally, we discuss how to generalize our approach to general semi-algebraic formulas.