I am looking for software that can find a global minimum of a polynomial function over a polyhedral domain (given by, say, some linear inequalities) in $\mathbb R^n$. 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.