SHF: Medium: Collaborative Research: Marrying Program Analysis and Numerical Search

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

• 批准号: 1162076
• 负责人: Swarat Chaudhuri
• 金额: $ 60万
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1162076&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搜索这样的黑盒优化技术原则上是适用的，但它们只在相对平滑的搜索空间中工作得很好，并且由于任意嵌套的分支和循环，即使是简单的程序也可能具有高度不规则性，不，引导这个项目的中心观点是，来自程序形式化推理领域的程序分析技术可以与黑盒优化一起工作工具包，并使之有可能解决更多的问题，上述排序比目前可能的。最终，该项目将产生一个用于优化程序的统一系统，该系统可以利用优化技术和程序分析策略的灵活组合。由于日常软件开发中面临的许多现实问题都是优化问题，因此该系统将为最终程序员提供一系列新的功能。此外，该研究将促进通常位于不同学术部门的两个不同研究领域之间的协同作用。