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.