nonlinear arithmetic

NIL: Learning Nonlinear Interpolants
Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model …
PDF Cite Code Slides DOI
NIL: Learning Nonlinear Interpolants
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and …
PDF Cite Code Slides DOI
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF