Verifying Relative Safety, Accuracy, and Termination for Program Approximations

Approximate computing is an emerging area for trading off the accuracy
of an application for improved performance, lower energy costs, and tolerance
to unreliable hardware. However, developers must ensure that the leveraged
approximations do not introduce significant, intolerable divergence from the reference
implementation, as specified by several established robustness criteria. In
this work, we show the application of automated differential verification towards
verifying relative safety, accuracy, and termination criteria for a class of program
approximations. We use mutual summaries to express relative specifications for
approximations, and SMT-based invariant inference to automate the verification
of such specifications. We perform a detailed feasibility study showing promise
of applying automated verification to the domain of approximate computing in a
cost-effective manner.