CS 590: Software Synthesis

TTh 12:00-1:15 LWSN B134

about

Instructor:

Ben Delaware

bendy at purdue.edu

Office Hours: By Appointment

Course Description:

Imagine a world in which you could simply tell your computer what problem a program should solve and have it write the program for you. Freed from the humdrum tasks of coding, you would be able focus on finding the right problems to solve (while also having more time to drink coffee). This is the dream of program synthesis: to automatically build implementations from high-level description of a program.

This seminar will begin with a broad overview of the field, including:

  1. how to learn a program from examples (inductive synthesis)
  2. how users can guide the search for an implementation (deductive synthesis)
  3. how to leverage cutting-edge theorem provers to find programs automatically

The second half of the course will focus on applications of synthesis to a variety of domains, including security, education, performance, and human computer interaction, with the specific topics tailored to participants' interests. Each unit will review the state of the art in the field with readings from the latest publications.

No previous knowledge is assumed, although experience with programming languages or machine learning is a plus. Auditors are welcome!

policies

Format:

This seminar course will be discussion-based: outside of introductory lectures by the instructor at the start of each unit, meetings will focus on discussing an assigned paper. Each paper will have a designated facilitator responsible for leading the discussion. To ensure a lively discussion, students will be responsible reading each day's paper and writing a short (.5 page) summary, reviewing the research problem, the proposed solution, the relationship to existing work, and the evaluation of any claimed contributions.

Reviews are to be submitted by posting a private note (the default setting) in the reviews folder on piazza . Students can either put their review directly in the post, or attach a file according to the instructions here.

Note to auditors: Glad to have you onboard! In order to fairly distribute the discussion workload, I ask that you lead one to two classes during the semester. Auditors are, of course, excused from turning reviews in, but everyone is encouraged to organize their thoughts about assigned papers in writing :)

Students will develop (in concert with the instructor) and work on an open-ended project over course of the semester. Ideally this will be an application of synthesis to their personal interests. Students are welcome to pair up for more ambitious projects. The project will include a short final report and presentation during the last week of class.

Discussion Forum:

The course piazza site will serve as the discussion board; all course announcements will also be posted there.

Grading:

Final grades will be assigned according to the following breakdown:

Class Project 40%
Paper Summaries 30%
Facilitating Discussion 15%
Participation 15%

tenative schedule

Date Topic
Week of 1/10
  • Course Introduction
  • Inductive Synthesis
Week of 1/17 No Class (POPL)
Week of 1/24
  • FlashRelate: Extracting Relational Data from Semi-Structured Spreadsheets Using Examples. Dan Barowy, Sumit Gulwani, Ted Hart, Benjamin Zorn.
  • Learning Programs from Noisy Data. Veselin Raychev, Pavol Bielik, Martin Vechev, Andreas Krause.
Week of 1/31
  • Type-and-Example-Directed Program Synthesis. Peter-Michael Osera, Steve Zdancewic.
  • Synthesizing Transformations on Hierarchically Structured Data. Navid Yaghmazadeh, Christian Klinger, Isil Dillig, Swarat Chaudhuri.
Week of 2/07
  • Intro to Deductive Synthesis
  • Deriving Divide-and-Conquer Dynamic Programming Algorithms using Solver-Aided Transformations. Shachar Itzhaky, Rohit Singh, Rezaul Chowdhury, Kuat Yessenov, Yongquan Lu, Charles E. Leiserson, Armando Solar-Lezama.
  • Project Prosoals Due (2/09)
Week of 2/14
  • Formal Derivation of Concurrent Garbage Collectors. Dusko Pavlovic, Peter Pepper, Douglas R. Smith.
  • Synthesis modulo recursive functions. Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, Philippe Suter.
Week of 2/21
  • LASE: Locating and Applying Systematic Edits by Learning from Examples. Na Meng, Miyrung Kim, Kathryn S. McKinley.
  • Combinatorial Sketching for Finite Programs. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, and Sanjit Seshia.
Week of 2/28
  • From Program Verification to Program Synthesis. Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster.
Week of 3/07 Synthesis for Performance
Week of 3/14 Spring Break
Week of 3/21 Midpoint Project Presentations
Week of 3/28 Synthesis for Performance
Week of 4/04 Synthesis for Education
Week of 4/11 Synthesis for Education
Week of 4/18 Synthesis for Security
Week of 4/25 Synthesis for Security
5/4 Final Reports Due

papers

  • Synthesis: Dreams -> Programs. Zohar Manna, Richard Waldinger.

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

  • FlashRelate: Extracting Relational Data from Semi-Structured Spreadsheets Using Examples. Dan Barowy, Sumit Gulwani, Ted Hart, Benjamin Zorn.

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

  • Recursive Program Synthesis. Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid.

  • Program sketching. Armando Solar-Lezama.

  • KIDS: A Semi-Automatic Program Development System. Douglas R. Smith.
  • Program Boosting: Program Synthesis via Crowd-Sourcing. Robert A Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar, Margus Veanes.

  • Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala.

  • Test-Driven Synthesis. Daniel Perelman, Sumit Gulwani, Dan Grossman, Peter Provost.

  • Code Completion with Statistical Language Models. Veselin Raychev, Martin Vechev, Eran Yahav.

  • Sumit Gulwani. Automating String Processing in Spreadsheets using Input-Output Examples.

  • Stochastic superoptimization. Eric Schkufza, Rahul Sharma, Alex Aiken.

  • Oracle-guided component-based program synthesis. Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari.

  • SPIRAL: Code Generation for DSP Transforms. Markus Püschel, José M. F. Moura, Jeremy Johnson, David Padua, Manuela Veloso, Bryan Singer, Jianxin Xiong, Franz Franchetti, Aca Gacic, Yevgen Voronenko, Kang Chen, Robert W. Johnson and Nicholas Rizzolo.

  • CodeHint: Dynamic and Interactive Synthesis of Code Snippets. Joel Galenson, Philip Reames, Rastislav Bodik, Björn Hartmann, Koushik Sen.

  • Programming by Manipulation for Layout. Thibaud Hottelier, Ras Bodik, Kimiko Ryokai.

  • Configuration Synthesis for Programmable Analog Devices with Arco. Sara Achour, Rahul Sarpeshkar, Martin Rinard.

  • MapReduce Program Synthesis. Calvin Smith, Aws Albarghouthi.

  • Programmatic and Direct Manipulation, Together at Last. Ravi Chugh, Brian Hempel, Mitchell Spradlin, Jacob Albers.

  • Fast Synthesis of Fast Collections. Calvin Loncaric, Emina Torlak, Michael D. Ernst.

  • Component-Based Synthesis for Complex APIs. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps.

  • Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks. Kausik Subramanian, Loris D'Antoni, Aditya Akella.

  • Optimizing Synthesis with Metasketches. James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze.

  • Maximal Specification Synthesis. Aws Albarghouthi, Isil Dillig, Arie Gurfinkel.

  • Example-Directed Synthesis: A Type-Theoretic Interpretation. Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic.

  • Decentralizing SDN Policies. Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham.

  • Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search. Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama.

  • A Constraint-Based Approach to Solving Games on Infinite Graphs. Tewodros Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko.

  • Sound Compilation of Reals. Eva Darulova, Viktor Kuncak.

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

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

  • Synthesizing racy tests. Malavika Samak, Murali Krishna Ramanathan, Suresh Jagannathan.

  • Synthesizing Data Structure Transformations from Input-Output Examples. John Feser, Swarat Chaudhuri, Isil Dillig.

  • Synthesizing Parallel Graph Programs via Automated Planning. Dimitrios Prountzos, Roman Manevich, Keshav Pingali.

  • Concurrency Debugging with Differential Schedule Projections. Nuno Machado, Brandon Lucia, Luís Rodrigues.

  • Synthesis of Machine Code from Semantics. Venkatesh Srinivasan, Thomas Reps.

  • Synthesis of ranking functions using extremal counterexamples. Laure Gonnord, David Monniaux, Gabriel Radanne.

  • FlashExtract : A Framework for Data Extraction by Examples. Vu Le, Sumit Gulwani.

  • Chlorophyll: Synthesis-Aided Compiler for Low-Power Spatial Architectures. Phitchaya Mangpo Phothilimthana, Tikhon Jelvis, Rohin Shah, Nishant Totla, Sarah Chasins, Rastislav Bodik.

  • Syntax-Guided Synthesis. Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak and Abhishek Udupa:

  • Growing Solver-Aided Languages with Rosette. Emina Torlak and Rastislav Bodik. Growi

  • Smten with satisfiability-based search. Richard Uhler, Nirav Dave.

  • User-Guided Device Driver Synthesis. Leonid Ryzhyk, Adam Walker, John Keys, Arun Raghunath, Michael Stumm, Mona Vij.

  • Synthesis modulo recursive functions. Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, Philippe Suter.

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

  • Abstraction-guided synthesis of synchronization. Martin Vechev, Eran Yahav, Greta Yorsh.

  • Formal Derivation of Concurrent Garbage Collectors. Dusko Pavlovic, Peter Pepper, and Douglas R. Smith.