I am looking for software that can find a global minimum of a polynomial function in R^n over a polyhedral domain (given by some linear inequalities say). The number of variables n is not more than a dozen. I know it can be done in theory (by Tarski's elimination of quantifiers in real closed fields), and I know that the time complexity is awful. However if there is a decent implementation that can handle a dozen variables with a clean interface, it would be great. I have tried builtin implementations in Mathematica and Maple, and they do not appear terminate on 4-5 variable instances.

If the software can produce some kind of concise "certificate" of its answer, it would be even better, but I am not sure how such a certificate should look like even in theory.

Edit: Convergence to the optimum is nice, but what I am really looking for is ability to answer questions of the form "Is minimum equal to 5?" where 5 is what I believe on a priori grounds to be the answer to optimization to be (in particular, it is a rational number). That also explains why I want a certificate/proof of the inequality, or a counterexample if it is false.