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

点击翻译按钮获取中文摘要

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.