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: TBA
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 automata-based synthesis, 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 it. The presentation will be followed by discussions.




 Reading



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

* Synthesis: Dreams -> Programs
   Zohar Manna, Richard Waldinger

* 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

* 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

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

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

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

* 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

* TRANSIT: Specifying Protocols with Concolic Snippets.
   PLDI 2013. A. Udupa, et. al..

And other papers that will be announced here.




 Extra Suggested Reading



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

* From Program Verification to Program Synthesis
   Saurabh Srivastava, Sumit Gulwani and Jeff Foster

* On the synthesis of a reactive module.
   POPL 1989. Amir Pnueli and Roni Rosner.

* Synthesis: Dreams -> Programs
   Zohar Manna, Richard Waldinger
  
* Program sketching
   Armando Solar-Lezama

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

* DemoMatch: API discovery from demonstrations
   PLDI 2017. Kuat Yessenov, Ivan Kuraj, Armando Solar-Lezama

* 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
   Sumit Gulwani

* FlashMeta: a framework for inductive program synthesis.
   OOPSLA 2015. Oleksandr Polozov and Sumit Gulwani.
     
* Type-and-Example-Directed Program Synthesis
   PLDI 2015. Peter-Michael Osera, Steve Zdancewic

* Program Synthesis from Polymorphic Refinement Types
   PLDI 2016. Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama

* Component-Based Synthesis for Complex APIs
   POPL 17. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps
     
* Complete functional synthesis
   PLDI 2010. Viktor Kuncak, Mikael Mayer, Ruzica Piskac, Philippe Suter

* Growing Solver-Aided Languages with Rosette
   Emina Torlak and Rastislav Bodik  

* Stochastic superoptimization.
   ASPLOS 2013. Eric Schkufza, Rahul Sharma, and Alex Aiken.
  
* Genetic programming - on the programming of computers by means of natural selection.
   MIT Press, 1993. John R. Koza.

* Programming by demonstration using version space algebra
   JML 2003. Tessa La, Steven A. Wolfman, Pedro Domingos, Daniel S. Weld

* Optimizing Synthesis with Metasketches
   POPL 16. James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze

* Bing developer assistant: improving developer productivity by recommending sample code.
   FSE 2016. Hongyu Zhang, Anuj Jain, Gaurav Khandelwal, Chandrashekha Kaushik,
   Scott Ge, Wenxiang Hu.
  
* Quantitative synthesis for concurrent programs.
   CAV 2011. Pavol Cerny, Krishnendu Chatterjee, Thomas A. Henzinger,
   Arjun Radhakrishna, and Rohit Singh.

* Measuring and synthesizing systems in probabilistic environments
   J. ACM 2015. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann,
   and Rohit Singh.

* Bridging boolean and quantitative synthesis using smoothed proof search.
   POPL 2014. Swarat Chaudhuri, Martin Clochard, and Armando Solar-Lezama.

* Fast Synthesis of Fast Collections
   PLDI 16. Calvin Loncaric, Emina Torlak, Michael D. Ernst

* Code Completion with Statistical Language Models
   PLDI 2014. Veselin Raychev, Martin Vechev, Eran Yahav

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

* Synthesizing memory models from framework sketches and Litmus tests
   PLDI 2017. James Bornholt, Emina Torlak

* Learning programs: A hierarchical Bayesian approach.
   ICML 2010. Percy Liang, Michael I. Jordan, and Dan Klein.

* A machine learning framework for programming
   ICML 2013. Aditya Krishna Menon, Omer Tamuz, Sumit Gulwani, Butler W. Lampson,
   Adam Kalai.

* Learning Programs from Noisy Data
   Veselin Raychev, Pavol Bielik, Martin Vechev, Andreas Krause

* DeepCoder: Learning to write programs.
   2016. Matej Balog, Alexander L. Gaunt, Marc Brockschmidt, Sebastian Nowozin,
   and Daniel Tarlow.

* Inductive logic programming.
   New generation computing 1991. Stephen Muggleton

* Program synthesis using natural language
   ICSE 2016. Aditya Desai, Sumit Gulwani, Vineet Hingorani, Nidhi Jain, Amey Karkare,
   Mark Marron, Sailesh R., and Subhajit Roy.

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

* Efficient Synthesis for Concurrency by Semantics-Preserving Transformations.
   CAV 2013. P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach.

* Regression-free Synthesis for Concurrency.
   CAV 2014. P. Cerny, et. al..

* From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis.
   CAV 2015. P. Cerny, et. al..

* Synthesis of Synchronization using Uninterpreted Functions.
   FMCAD 2014. R. Bloem, G. Hofferek, B. Konighofer, R. Konighofer,
   S. Ausserlechner, R. Spork.

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

* Automatic inference of memory fences.
   FMCAD 2010. Michael Kuperstein, Martin T. Vechev, and Eran Yahav

* Declarative fence insertion
   OOPSLA 2015. John Bender, Mohsen Lesani, Jens Palsberg  

* TRANSIT: Specifying Protocols with Concolic Snippets.
   PLDI 2013. A. Udupa, et. al..

* MSL: A Synthesis Enabled Language for Distributed Implementations.
   SC 2014. Z. Xu, S. Kamil, A. Solar-Lezama.

* SMT-Based Synthesis of Distributed Self-Stabilizing Systems.
   TAAS 2015. Fathiyeh Faghih, Borzoo Bonakdarpour

* Symbolic synthesis of masking fault-tolerant distributed programs.
   Distributed Computing 2012. Borzoo Bonakdarpour, Sandeep S. Kulkarni, Fuad Abujarad
     
* Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems.
   CAV 2016. Roderick Bloem, Nicolas Braud-Santoni, Swen Jacobs
     
* Distributed synthesis is simply undecidable.
   IPL 2014, Sven Schewe.
     
* Automatic Discovery of Mutual Exclusion Algorithms.
   DISC 2003. Y. Bar-David, G. Taubenfeld.     

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

* Abstraction-Guided Synthesis of Synchronization.
   POPL 2010. M. Vechev, E. Yahav, G. Yorsh.     

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

* Leveraging Parallel Data Processing Frameworks with Verified Lifting.
   Synth Workshop 2016. M. Ahmed, A. Cheung.

* Optimizing database-backed applications with query synthesis.
   PLDI 13. Alvin Cheung, Armando Solar-Lezama, and Samuel Madden.

* Query by Output.
   SIGMOD 2008. Q. Tran, S. Parthasarathy.

* Automatically Synthesizing SQL Queries from Input-output Examples.
   ASE 2013. S zhang, Y. Sun.

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




 Evaluation



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