EAGER: Duality-Based Algorithm Synthesis

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

The task of designing an algorithm that performs a desired function, or achieves a desired goal, currently requires expertise in the problem domain. Consequently, although people have access to powerful computing platforms, most non-experts are limited to using these platforms through pre-programmed apps. Automated program synthesis changes this current state of affairs by enabling computers to convert high-level specification of the problem to a computable procedure. Apart from the benefit of making technology accessible to more people, program synthesis has the promise of reducing errors, and improving performance, of software. Program synthesis refers to the problem of discovering a program that meets the requirements specified by a user. It is a hard problem to solve in general. However, if the space of possible programs is restricted, then it becomes feasible to iteratively search the space of possible programs for some program that works correctly on all inputs. The quantifier alternation in this exists-forall formulation makes synthesis computationally difficult and hinders scalability. This project drastically improves efficiency of program synthesis by developing and exploiting a notion of duality in programming. Duality between computing and proving promises to play a foundational role in understanding program analysis and synthesis. It not only encompasses several well-known concepts, such as types, abstractions, and abstract interpretation, but also goes beyond them to provide a general methodology for attaching a proof with a program. Duality enables approximating the exists-forall synthesis constraint by a relatively more tractable exists-constraint. This project develops the duality-based synthesis approach. This project also makes contributions to education, research, and technology transfer to industry through freely distributed tools and academic visitor programs that include internships for graduate students.