A theorem prover specialised in deciding inequalities of non-linear real and floating-point expressions using rigorous polynomial approximations.  Includes tools for verifying floating-point SPARK 2005 programs.