Program Synthesis

ECEN 5033, CSCI 7000-007

Information

Lectures Tue, Thu 11-12.15 in ECEE 265
Instructor Pavol Cerny, office hours: Thu 2-3pm in ECOT 349, and by appointment

Course description

Computer-aided programming, or partial-program synthesis, is emerging as an effective approach for increasing programmer productivity. Its goal is to harness the improvements in constraint-solving technology and the increase in routinely available computational power in order to enable programmers to express insights in a variety of forms such as incomplete programs, example behaviors, and high-level requirements. In the course, we will cover the foundations, as well as current research and prototype tools.

Course topics

What can you expect to get out of the course:
  • Practical experience with partial-program synthesis
  • View of the landscape:
    • Partial-program synthesis
    • Counterexample-guided synthesis
    • Inductive synthesis
    • Classical synthesis, Church's problem
    • Synthesis from LTL
    • Synthesis and Games
    • Deductive synthesis
    • Quantitative synthesis
  • Learn about technical topics useful in synthesis, verification, program analysis; as needed:
    • specification logics
    • constraint solving (SAT, SMT)
    • abstract interpretation
Advertisement/warning: This is a class on a very recent research topic. Expect to read research papers.

Schedule

January 15 : Introduction; What is synthesis; Demos of synthesis in action. Slides.

January 17 : Partial-program synthesis: Counterexample-guided inductive synthesis (CEGIS).
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, Sanjit A. Seshia. Combinatorial Sketching for Finite Programs. Proceedings of ASPLOS 2006.

January 22, 24 : Instructor away (POPL conference).

January 29, 31: Partial-program synthesis: CEGIS for concurrency.
Armando Solar-Lezama, Christopher G. Jones, Rastislav Bodik, Sketching Concurrent Data Structures, Proceedings of PLDI 2008.
Martin Vechev, Eran Yahav, Greta Yorsh. Abstraction-Guided Synthesis of Synchronization. Proceedings of POPL 2010.

February 5: Partial-program synthesis: an application of CEGIS.
Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, Sanjit Seshia. Sketching Stencils. Proceedings of PLDI 2007.

February 7, 12: Implicit Programming.
Viktor Kuncak, Mikael Mayer, Ruzica Piskac, and Philippe Suter. Complete functional synthesis. Proceedings of PLDI 2010.
Ali Sinan Koksal, Viktor Kuncak, and Philippe Suter. Constraints as control. Proceedings of POPL 2012.

February 14:
Saurabh Srivastava, Sumit Gulwani, Jeff Foster. From Program Verification to Program Synthesis. Proceeedings of POPL 2010.

February 19, 21: Synthesis using version-space algebras.
Sumit Gulwani. Automating String Processing in Spreadsheets using Input-Output Examples. Proceeedings of POPL 2010.
William Harris, Sumit Gulwani. Spreadsheet Table Transformations from Examples. Proceeedings of PLDI 2011.
Rishabh Singh, Sumit Gulwani. Learning Semantic String Transformations from Examples. Proceeedings of VLDB 2012.

February 26, 28, March 5, 7, 12: Synthesis for (concurrent) data structures.
Martin Vechev, Eran Yahav. Deriving linearizable fine-grained concurrent objects. Proceeedings of PLDI 2008.
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard, Mooly Sagiv. Data Representation Synthesis. Proceedings of PLDI 2011.
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard, Mooly Sagiv. Concurrent Data Representation Synthesis. Proceedings of PLDI 2012.
Ohad Shacham, Martin Vechev, Eran Yahav. Chameleon: Adaptive Selection of Collections. Proceeedings of PLDI 2009.
Rishabh Singh, Armando Solar-Lezama. Synthesizing Data-structure Manipulations from Storyboards . Proceeedings of FSE 2011.

March 14: Guest lecture by Sriram Sankaranarayanan.
Sanjit Seshia, Alexander Rakhlin. Quantitative Analysis of Systems Using Game-Theoretic Learning. ACM Transactions on Embedded Computing Systems (TECS), 2012.

March 19:
Rastislav Bodik, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, Casey Rodarmor. Programming with angelic nondeterminism. Proceedings of POPL 2010.

March 21:
Ali Sinan Koksal, Yewen Pu, Saurabh Srivastava, Rastislav Bodik, Jasmin Fisher, Nir Piterman. Synthesis of Biological Models from Mutation Experiments. Proceedings of POPL 2013.

April 2,4,9: Student presentations.
Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac. On Complete Completion using Types and Weights. PLDI 2013, to appear. Presented by Sam.
Ankur Taly, Sumit Gulwani, Ashish Tiwari. Synthesizing switching logic using constraint solving. STTT, 13(6). Presented by Hadi.
Holger Hermanns, Bjoern Wachter, and Lijun Zhang. Probabilistic CEGAR. CAV 2008. Presented by Aleks.

April 11:
Zohar Manna, Richard Waldinger. Toward Automatic Program Synthesis. Communications of the ACM 14(3), 1971.

April 16:
Amir Pnueli, Roni Rosner. On the Synthesis of a Reactive Module. Proceedings of POPL 1989.

April 18,23:
Nir Piterman, Amir Pnueli, Yaniv Sa'ar. Synthesis of Reactive(1) Designs. Proceedings of VMCAI 2006.
See also lectures by Barbara Jobstmann.

April 25:
Marcin Jurdzinski, Mike Paterson, Uri Zwick. A deterministic subexponential algorithm for solving parity games.. Proceedings of SODA 2006.

April 30: Overview of formalizations and algorithms.
Sumit Gulwani. Dimensions in Program Synthesis. Proceedings of PPDP 2010.

May 2:
Project presentations.



Course project

The goal of your project is to build a synthesizer for a domain of your choice (ideally, related to your research interests). Project deadlines:
  • February 19: project proposal
  • April 2: checkpoint (project works on motivating examples)
  • April 30: project submission deadline (submit source code, examples, project report)
  • May 2: project presentations, demos

Relevant links

Tutorial by Ras Bodik.
LNCS 2500 : Automata, Logics, and Infinite Games: A Guide to Current Research
Recent large research project on synthesis.


Grading

The course will be graded based on a course project(50% of the course grade), in class presentations (40%), and class participation (10%).

Syllabus statement

A statement of class policies is available here.