Program Synthesis with Lightweight Abstractions

The world is increasingly reliant on software systems of unprecedented scale, while our methods for developing software still require programmers to manually write code with little help in ensuring software correctly meets its intent. Program synthesis, which automatically generates correct programs from specifications, offers a hopeful path forward. While program synthesis has had many successes in recent years, these have mostly been in restricted domains; synthesis has not yet proved useful for the practicing software engineer.This dissertation advances the science of program synthesis to meet the challenges posed by the use of modern general-purpose languages, tools, and frameworks. In this talk, I will present a work towards an automated programming stack that uses specifications and expressive test cases written by programmers to scale synthesis tools to diverse domains. Specifically, I show that types enriched with effect descriptors inferred from test cases are a potent means to guide the synthesis of real Ruby on Rails web apps or types enriched with logical predicates can be used to synthesize verified privacy preserving queries. The key to both projects, and most other successful synthesis work, is the proper choice of abstraction for the problem domain at hand. Based on this insight, I will describe a new synthesis framework that captures many different synthesis approaches from the literature, making it easier to build the synthesis tools of the future. Finally, I will present a vision for an automated programming stack that uses specifications and expressive test cases written by programmers to scale synthesis tools to diverse domains, moving us closer to a world in which correct programs are constructed automatically from a programmer's intent.

Examining Committee

Chair:

Dr. David Van Horn

Co-Chair:
Dean's Representative:

Dr. Jeffrey S. Foster (Tufts)
Dr. Lawrence Washington

Members:

Dr. Mike Hicks

Dr. Leonidas Lampropoulos