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, 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.
Citation
Shaobo He,
Shuvendu K. Lahiri,
Zvonimir Rakamaric
Verifying Relative Safety, Accuracy, and Termination for Program Approximations
Proceedings of the 8th NASA Formal Methods Symposium (NFM), 9690: 237--254, doi:10.1007/978-3-319-40648-0_19, 2016.
BibTeX
@inproceedings{2016_nfm_hlr,
title = {Verifying Relative Safety, Accuracy, and Termination for Program Approximations},
author = {Shaobo He and Shuvendu K. Lahiri and Zvonimir Rakamaric},
booktitle = {Proceedings of the 8th NASA Formal Methods Symposium (NFM)},
series = {Lecture Notes in Computer Science},
volume = {9690},
publisher = {Springer},
editor = {Sanjai Rayadurgam and Oksana Tkachuk},
pages = {237--254},
doi = {10.1007/978-3-319-40648-0_19},
year = {2016}
}
Acknowledgements
We thank Adrian Sampson for his feedback and for helping out with benchmark selection, and Akash Lal for helping out with Houdini. This work was supported in part by NSF award CCF 1255776 and SRC contract 2013-TJ-2426.