@inproceedings{MFK+16,
title = { Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem },
author = {Mar\'echal, Alexandre and Fouilh\'e, Alexis and King, Tim and Monniaux, David and P'erin, Micha\"el},
month = {jan},
year = {2016},
booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
eprint = {hal-01223362},
pages = {166--184},
volume = {9583},
team = {PACSS},
timestamp = {Tue, 05 Jan 2016 12:40:34 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/MarechalFKMP16},
bibsource = {dblp computer science bibliography, http://dblp.org},
eprinttype = {HAL},
entrysubtype = {intc},
abstract = {Convex polyhedra are commonly used in the static analysis of programs to represent over-approximations of sets of reachable states of numerical program variables. When the analyzed programs contain nonlinear instructions, they do not directly map to standard polyhedral operations: some kind of linearization is needed. Convex polyhe-dra are also used in satisfiability modulo theory solvers which combine a propositional satisfiability solver with a fast emptiness check for polyhedra. Existing decision procedures become expensive when nonlinear constraints are involved: a fast procedure to ensure emptiness of systems of nonlinear constraints is needed. We present a new linearization algorithm based on Handelman's representation of positive polynomials. Given a polyhedron and a polynomial (in)equality, we compute a polyhedron enclosing their intersection as the solution of a parametric linear programming problem. To get a scalable algorithm, we provide several heuristics that guide the construction of the Handelman's representation. To ensure the correctness of our polyhedral approximation , our Ocaml implementation generates certificates verified by a checker certified in Coq.},
}
