|Lectures||Tue, Thu 11-12.15 in ECEE 265|
|Instructor||Pavol Cerny, office hours: Thu 2-3pm in ECOT 349, and by appointment|
Course descriptionComputer-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 topicsWhat 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
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.
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.
Rastislav Bodik, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, Casey Rodarmor. Programming with angelic nondeterminism. Proceedings of POPL 2010.
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.
Zohar Manna, Richard Waldinger. Toward Automatic Program Synthesis. Communications of the ACM 14(3), 1971.
Amir Pnueli, Roni Rosner. On the Synthesis of a Reactive Module. Proceedings of POPL 1989.
Nir Piterman, Amir Pnueli, Yaniv Sa'ar. Synthesis of Reactive(1) Designs. Proceedings of VMCAI 2006.
See also lectures by Barbara Jobstmann.
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.
- 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 linksTutorial by Ras Bodik.
LNCS 2500 : Automata, Logics, and Infinite Games: A Guide to Current Research
Recent large research project on synthesis.