Verimag

bibtex

@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.},
}

URL

Publication Sections


Contact | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 876140