Towards Automated Differential Program Verification for Approximate Computing

Shuvendu K. Lahiri, Zvonimir Rakamaric. Workshop on Approximate Computing Across the Stack (WAX 2015), Portland, OR, USA.
[pdf] [bib]

Abstract: 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, care has to be taken to ensure that the approximations do not cause significant divergence from the reference implementation. Previous research has proposed various metrics to guarantee several relaxed notions of safety for the design and verification of such approximate applications. However, current approximation verification approaches often lack in either precision or automation. On one end of the spectrum, type-based approaches lack precision, while on the other, proofs in interactive theorem provers require significant manual effort. In this work, we apply automated differential program verification (as implemented in SymDiff) for reasoning about approximations. We show that mutual summaries naturally express many relaxed specifications for approximations, and SMT-based checking and invariant inference can substantially automate the verification of such specifications. We demonstrate that the framework significantly improves automation compared to previous work on using Coq. Our results indicate the feasibility of applying automated verification to the domain of approximate computing in a cost-effective manner.

Bibtex:

@inproceedings{wax2015-lr,
  author = {Shuvendu K. Lahiri and Zvonimir Rakamari\'c},
  title = {Towards Automated Differential Program Verification for Approximate Computing},
  booktitle = {Informal Proceedings of the Workshop on Approximate Computing Across the
    Stack (WAX)},
  year = {2015},
  note = {Position paper},
}