CAREER: Formal Methods for Approximate Computing

如今，功率和能量约束是提高计算能力的主要驱动力，而近似计算已经成为实现这些改进的一种有前途的技术。 近似计算背后的主要思想是以计算的准确性为代价，以实现新的优化，从而提高性能或能源效率。 这利用了许多应用程序在某种程度上对错误具有弹性的事实，因此不需要绝对正确的计算。显然，为未来的近似计算平台开发软件将不是一件容易的事：开发人员必须引入尽可能多的近似，同时确保应用程序的正确性和结果质量要求得到满足。这个项目探索了自动化技术和工具，以帮助开发人员探索近似计算的权衡。这些技术是基于一个严格的，自动化的，和精确的分析，地图proximations。主要的新奇是利用最近的进展，在自动化软件验证的近似计算的背景下。该项目将为近似程序的严格分析开发一个开放平台。 通过专注于改善开发人员在为未来近似计算平台编写代码时的体验，这项工作有可能在广泛的行业和应用程序中产生重大影响。

Nowadays, power and energy constraints are the main driving force ofimprovements in computing abilities, and approximate computing has emerged as apromising technique for enabling these improvements. The main idea behindapproximate computing is to trade the accuracy of computations in order toenable novel optimizations that improve performance or energy efficiency. Thisleverages 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 timeensuring that correctness and the results quality requirements of anapplication are met.This project explores automated techniques and tools to assist developers byallowing them to explore approximate computing trade-offs. The techniques arebased around a rigorous, automated, and precise analysis of programapproximations. The main novelty is to leverage recent advances in automatedsoftware verification in the context of approximate computing. The project willdevelop 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.