  In order to verify programs or hybrid systems, one often needs to prove that
certain formulas are unsatisfiable. In this paper, we consider conjunctions of
polynomial inequalities over the reals. Classical algorithms for deciding these
not only have high complexity, but also provide no simple proof of
unsatisfiability. Recently, a reduction of this problem to semidefinite
programming and numerical resolution has been proposed. In this article, we
show how this reduction generally produces degenerate problems on which
numerical methods stumble.
