CS 590: Software Synthesis
|
about
Instructor:
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:
- how to learn a program from examples
(inductive synthesis)
- how users can guide the search for an
implementation (deductive synthesis)
- 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.
|
|
|