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.

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