COMP 607: Program Synthesis: Spring 2015
Software synthesis has been one of the holy grails of computer science since the late 60s; it was considered by Pnueli to be "one of the most central problems in the theory of programming." The promise of synthesis is that we should be able to tell the computer what to do, and let the synthesizer discover how to do it. From a specification, the synthesizer should automatically (or at least mechanically) produce a correct and efficient implementation. The last few years have seen software synthesis emerge as one of the hottest areas in programming languages and formal methods.
The seminar will serve as a participatory introduction to this dynamic research area. We will study a series of papers on software synthesis, including deductive synthesis, constraint-based synthesis, automata-based synthesis, and quantitative synthesis.
This seminar meets at DH 1046. The regular time slot for the seminar is Monday, 3:00-4:30pm, but we reserve also Friday, 3:00-4:30, to cover cases when the Monday slot conflicts with another event.
We will read 14 papers, including classic as well as recent articles, on program synthesis. We will treat these papers as if they have been submitted to a conference whose program committee consists of COMP 607 participants.
Participants will be expected to prepare a review of the “paper of the week” before coming to class. The reviews should be similar in style and scope to reviews in top-tier computer science conferences. The reviews will have to be entered through the Easychair system.
In each class, we will have a 30-minute summary of the paper by a “discussion leader” (a rotating position), followed by a discussion. Each reviewer will articulate their thoughts on the strengths and weaknesses of the paper.
Resources on paper reviews
Here are a couple of resources on how to write reviews of technical papers.
Here are the papers that we will study in the seminar.
Zohar Manna, Richard J. Waldinger: Fundamentals of Deductive Program Synthesis. IEEE Trans. Software Eng. 18(8)
Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh,Armando Solar-Lezama, Emina Torlak, Abhishek Udupa: Syntax-guided synthesis. FMCAD 2013
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, Vijay A. Saraswat: Combinatorial sketching for finite programs. ASPLOS 2006
Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter: Complete functional synthesis. PLDI 2010
Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster: Template-based program verification and program synthesis. STTT 15(5-6)
Sumit Gulwani, Vijay Anand Korthikanti, Ashish Tiwari: Synthesizing geometry constructions. PLDI 2011