Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues wit h classical decision procedures are still a major obstacle for formal verificati on of real-world applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic tec hniques and implementations for the universal fragment of real-closed fields: ap proaches based on quantifier elimination, Gr{\"o}bner Bases, and semidefinite pr ogramming for the Positivstellensatz. Within a uniform context of the verification tool \KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybr id systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gr{\"o}bner Bases and semidefinite programming for the real Nullstellensatz that outperforms the indi vidual approaches on an interesting set of problems.