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