Duality-Based Algorithm Synthesis (NSF EAGER)
Abstract: 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.
Technical Director, NuSCI
My research interests include artificial intelligence, formal methods, machine learning and dynamical systems.