CAREER: Formal Methods for Approximate Computing

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

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.