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

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

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.