Nowadays, power and energy constraints are the main driving force of improvements in computing abilities, and approximate computing has emerged as a promising technique for enabling these improvements. The main idea behind approximate computing is to trade the accuracy of computations in order to enable novel optimizations that improve performance or energy efficiency. This leverages the fact that many applications are resilient to errors to some extent, and hence do not require absolute correctness of computations. Clearly, developing software for future approximate computing platforms will not be an easy task: a developer must introduce as many approximations as possible, while at the same time ensuring that correctness and the results quality requirements of an application are met.
This project explores automated techniques and tools to assist developers by allowing them to explore approximate computing trade-offs. The techniques are based around a rigorous, automated, and precise analysis of program approximations. The main novelty is to leverage recent advances in automated software verification in the context of approximate computing. The project will develop an open platform for the rigorous analysis of approximate programs. By focusing on improving developer's experience when writing code for future approximate computing platforms, this work has the potential to achieve significant impact across a wide spectrum of industries and applications.
