SHF: Medium: Collaborative Research: Marrying program analysis and numerical search

SHF：媒介：协作研究：结合程序分析和数值搜索

• 批准号: 1161775
• 负责人: Armando Solar-Lezama
• 金额: $ 60万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1161775&HistoricalAwards=false
• 关键词: SHF; Medium; Collaborative; Research; Marrying

This research project explores ways to solve optimization problems where the targets of optimization are programs containing general-purpose control and data constructs. Such optimization questions arise often in the everyday practice of software engineering. While it may seem that standard optimization packages could solve these problems, it is often not so. White-box optimization approaches like linear programming are ruled out here because they only permit very restricted classes of objective functions. Black-box optimization techniques like gradient descent and Nelder-Mead search are applicable in principle, but they work well only in relatively smooth search spaces, and due to arbitrarily nested branches and loops, even simple programs can have highly irregular, ill-conditioned behavior.The central insight guiding this project is that program analysis techniques from the field of formal reasoning about programs can work together with blackbox optimization toolkits, and make it possible to solve many more problems of the above sort than are currently possible. Ultimately, the project will produce a unified system for optimizing programs that can leverage flexible combinations of optimization techniques and program analysis strategies. As numerous real-world problems faced in the development of everyday software are optimization problems, this system will offer a new range of capabilities to the end programmer. In addition, the research will foster synergy between two different research areas customarily housed in different academic departments.

该研究项目探索解决优化问题的方法，其中优化目标是包含通用控制和数据结构的程序。此类优化问题经常出现在软件工程的日常实践中。虽然标准优化包似乎可以解决这些问题，但事实往往并非如此。这里排除了线性规划等白盒优化方法，因为它们只允许非常有限的目标函数类别。梯度下降和 Nelder-Mead 搜索等黑盒优化技术原则上是适用的，但它们只能在相对平滑的搜索空间中有效，并且由于任意嵌套的分支和循环，即使是简单的程序也可能具有高度不规则、病态的行为。指导该项目的中心思想是来自程序形式推理领域的程序分析技术可以与黑盒优化工具包一起工作，并使得解决更多的问题成为可能。 以上排序比当前可能的排序要多。最终，该项目将产生一个统一的程序优化系统，可以利用优化技术和程序分析策略的灵活组合。由于日常软件开发中面临的许多现实问题都是优化问题，因此该系统将为最终程序员提供一系列新的功能。此外，该研究还将促进通常位于不同学术部门的两个不同研究领域之间的协同作用。