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.