COMP 607: Program Synthesis: Spring 2015

Course description

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.


Swarat Chaudhuri (swarat at and Moshe Vardi (vardi at


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.

Deductive synthesis

  • Zohar Manna, Richard J. Waldinger: Fundamentals of Deductive Program Synthesis. IEEE Trans. Software Eng. 18(8)

  • Constraint-based synthesis

  • 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

    Inductive synthesis

    • Emanuel Kitzelmann and Ute Schmid: Inductive Synthesis of Functional Programs: An Explanation Based Generalization Approach
    • Sumit Gulwani: Automating string processing in spreadsheets using input-output examples. POPL 2011

    Automata-based synthesis

    • Amir Pnueli, Roni Rosner: On the Synthesis of a Reactive Module. POPL 1989
    • Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem: Program Repair as a Game. CAV 2005

    Solver-aided languages

    • Emina Torlak, Rastislav Bodík: A lightweight symbolic virtual machine for solver-aided host languages. PLDI 2014

    Quantitative synthesis

    • John von Neumann. Probabilistic logics and the synthesis of reliable organisms from unreliable components.
    • Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh: Measuring and Synthesizing Systems in Probabilistic Environments. CAV 2010
    • Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama: Bridging boolean and quantitative synthesis using smoothed proof search. POPL 2014