Nonlinear Craig Interpolant Generation

Craig interpolant generation for non-linear theory and its combination with other theories are still in infancy, although interpolation-based techniques have become popular in the verification of programs and hybrid systems where non-linear expressions are very common. 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\ge 0\wedge \cdots \wedge f_n\ge 0$ , 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 ( $\mathrm{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 $\mathrm{SDP}$ solving. Besides, we discuss how to generalize our approach to general semi-algebraic formulas. Finally, as an application, we demonstrate how to apply our approach to invariant generation in program verification.