Home / Teaching / CS 260

 CS 260: Seminar in Program Synthesis

 General Information     

Instructor: Mohsen Lesani
Instructor's email: lesani@cs.ucr.edu
Lecture time: Tuesday and Thursday 5:10 - 6:30 pm
Lecture room: Gordon Watkins Hall 117
Prerequisites: No previous knowledge is assumed, although experience with programming languages or machine learning is a plus.


 Course Description

Synthesis is to automatically build implementations from high-level descriptions of programs. The ambitious goal is to to tell the computer what to do, and let it find how to do it. Software synthesis is an emerging field at the intersection of programming systems, formal methods and artificial intelligence. The goal of this course is to provide broad overview of the field including deductive synthesis, inductive synthesis, synthesis from program sketches, search techniques to explore large spaces of candidate programs and applications of synthesis. We will review the state of the art by readings the latest publications.

Each class will have a presentation and discussion of a paper. Participants will be expected to prepare and submit a review of the paper before the class. Each paper will be assigned to a student to present. The presentation will be followed by discussions.


* Program Synthesis, Book
   2017. S. Gulwani, O. Polozov, R. Singh.

* Syntax-Guided Synthesis.
   FMCAD 2013. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin,
   Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama,
   Emina Torlak and Abhishek Udupa

* Automating String Processing in Spreadsheets using Input-Output Examples.
   POPL 2011. Sumit Gulwani

* Combinatorial Sketching for Finite Programs.
   ASPLOS 2006. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik,
   Vijay Saraswat and Sanjit Seshia

* Synthesis: Dreams -> Programs.
   IEEE Transactions on Software Engineering 1979. Zohar Manna, Richard Waldinger

* MapReduce Program Synthesis.
   PLDI 2016. C. Smith, A. Albarghouthi.

* Synthesizing highly expressive SQL queries from input-output examples.
   PLDI 2017. Chenglong Wang, Alvin Cheung, Rastislav Bodik

* Data Representation Synthesis.
   PLDI 2011. P. Hawkins, A. Aiken, K. Fisher. M. Rinard, M. Sagiv.

* Concurrent Data Representation Synthesis.
   PLDI 2012. P. Hawkins, A. Aiken, K. Fisher, M. Rinard, M. Sagiv.

* Declarative Programming over Eventually Consistent Data Stores.
   PLDI 2015. KC Sivaramakrishnan, G. Kaki, S. Jagannathan

* Sketching Concurrent Data Structures.
   PLDI 2008. A. Solar-Lezama, C. G. Jones, R. Bodik.

* Declarative Fence Insertion.
   OOPSLA 2015. John Bender, Mohsen Lesani, Jens Palsberg 

* Network configuration synthesis with abstract topologies.
   PLDI 2017. Ryan Beckett, Ratul Mahajan, Todd D. Millstein, Jitendra Padhye, David Walker

* Network-Wide Configuration Synthesis.
   CAV 2017. Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin Vechev.

* Synthesizing Parallel Graph Programs via Automated Planning.
   PLDI 2015. D. Prountzos, R. Manevich, K. Pingali.

* TRANSIT: Specifying Protocols with Concolic Snippets.
   PLDI 2013. A. Udupa, A. Raghavan, J. V. Deshmukh, S. Mador-Haim,
   M. Martin, R. Alur

* Quantitative synthesis for concurrent programs.
   CAV 2011. Pavol Cerny, Krishnendu Chatterjee, Thomas A. Henzinger,
   Arjun Radhakrishna, and Rohit Singh.

* A Simple Inductive Synthesis Methodology and its Applications.
   OOPSLA 2010. S. Itzhaky, S. Gulwani, N. Immerman

Extra Suggested reading


Participation and discussion: 20%
Presentation: 40%
Reviews: 40%