Research Projects

Program Synthesis

Ras Bodik

National Science Foundation, Intel and Microsoft

What computational technologies support programmers in the task of building complex systems? So far, four technologies have been adopted: testing, type checking, model checking, and compilers. First three focus on assuring correctness of code; compilers actually help with writing the code, by raising the level of programming abstractions. Despite adoption of high-level languages, though, it is fair to say that we don't know how to usefully burn computer cycles at the frontend of the program development process: programmers still rely on paper and pencil when writing code. We are developing computer-aided programming that brings the computational power to the process of constructing programs. We pose the problem as synthesis of programs from multi-modal specifications: templates of programs, declarative assertions, executable specifications, examples and demonstrations. We are developing synthesis theories and algorithms, language constructs and tools that embed synthesis into the programming process.