LifeJacket: Verifying precise floating-point optimizations in LLVM

Andres Nötzli, Fraser Brown

Optimizing floating-point arithmetic is vital because it is ubiquitous, costly, and used in compute-heavy workloads. Implementing precise optimizations correctly, however, is diffi…