Approximate Program Synthesis using Grenade

Real-number programs are at the core of much of computer science. Such programs are almost universally implemented using finite-precision approximations, such as fixed- or floating-point numbers, for reasons of both computability and efficiency. Approximation does not have to stop with fixed- or floating-point numbers: recent research has shown that additional approximations --- such as omitting loop iterations or using less preciseimplementations of certain core functions --- can greatly improve performance while still maintaining reasonable error bounds in many situations. A key difficulty in using approximations, however, is verifying approximated programs.  This requires proving that an approximated program is quantifiably correct with respect to the original, a more complex proof obligation than traditional program correctness.

In this paper, we address this difficulty with a new approach called approximate program synthesis where approximate programs are synthesized from real-number specification programs. Synthesized programs are guaranteed by construction to be quantifiably correct, given user-specified error bounds on their specifications, while opportunistically using approximations wherever possible, given these error bounds.