This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).
In contrast to software verification, software synthesis "writes" programs rather than merely checks them for errors. While verification has recently reached the programmer, the success of synthesis remains in the hands of formally trained experts. To ease the adoption of synthesis, this proposal develops algorithmic synthesis, which is to deductive synthesis what model checking is to deductive verification: Rather than deducing a program with a theorem prover, algorithmic synthesis systematically finds the program in a space of candidate implementations.
A key remaining challenge is how to describe this candidate space. Each synthesizer must be "programmed" with insights about the domain and its implementation tricks. In deductive synthesis, the insight is conveyed by a domain theory. In algorithmic synthesis, programmers typically communicate their insight by writing a partial program that syntactically defines the candidate space. The partial program is then completed by the synthesizer. Since the program is specified partially, programmers can control the candidate space size, making algorithmic synthesis feasible while leaving tedious program details to the synthesizer.
This project investigates linguistic aspects of algorithmic synthesis, addressing three issues: (1) How to debug partial programs? Angelically non-deterministic oracles will be used for gradual development of partial programs. (2) What is domain insight and how to communicate it? Programming abstractions will be developed for defining the candidate space naturally. (3) How to refine the insight with the goal of aiding the synthesizer scalability? An interactive dialogue between the programmer and the synthesizer will help the programmer refine and formalize her insight.
