Alexandre Maréchal, Michaël Périn
Three linearization techniques for multivariate polynomials in static analysis using convex polyhedra (2014)
Three linearization techniques for multivariate polynomials in static analysis using convex polyhedra (2014)
TR-2014-7.pdf
Keywords: polyhedra, linearisation, polynomials, Coq proof
Abstract: We present three linearization methods to over-approximate non-linear multivariate polynomials with convex polyhedra. The first one is based on the substitution of some variables by intervals. The principle of the second linearization technique is to express polynomials in the Bernstein basis and deduce a polyhedron from the Bernstein coefficients. The last method is based on Handelmans theorem and consists in using products of constraints of a given polyhedron to over-approximate a polynomial. As this work is part of the VERASCO project, the goal is to certify the methods with the Coq proof assistant.
