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 [Formula: see text] exists for two mutually contradictory polynomial formulas [Formula: see text] and [Formula: see text], with the form [Formula: see text], where [Formula: see text] are polynomials in [Formula: see text] or [Formula: see text], and the quadratic module generated by [Formula: see text] is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem ([Formula: see text]). 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 [Formula: see text] 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.