Automatic generation of proofs of arithmetic properties

 Tool to help verify and prove properties on numerical
 programs dealing with either fixed-point or floating-point
 arithmetic.