The pitfalls of verifying floating-point computations | Synapse