Program verification and synthesis aim to make programming a collaboration between developers and automated tools. They can help programmers produce high-quality code in less time, by checking that existing code satisfies important properties, or by creating new programs from multi-modal descriptions of the programmer's intent, such as program sketches, reference implemenations, and input/output examples. In this course, we will study recent advances in synthesis and verification, with the goal of developing tools to tackle new and exciting research problems!

Time
Tuesdays and Fridays, 1:30-2:30 pm
Place
CSE 110
Instructor
Emina Torlak (office hours by appointment)
Resources

Lectures

Lectures will primarily serve as collaborative teaching, learning, and discussion sessions. We will use them to explore technical details of research papers from the course reading list. The papers will be presented by students, and the instructor will help with the preparation.

You should read each assigned paper before the lecture. If you are the presenter, email a draft of your presentation materials (i.e., notes and, optionally, slides) to the instructor 48 hours before the lecture. Otherwise, submit (via email) a one-paragraph summary of the paper, together with a list of questions for in-class discussion. Reading summaries and questions are due at midnight before the lecture.

Projects

During the quarter, you will work on developing a novel verification or synthesis tool for a domain of your choice. You may work in teams or on your own. The project should be related to your research—ideally, it will be your research for the quarter!

The goal of the project is to produce a prototype tool and aim toward publishing the work in a conference or a workshop paper. To that end, we will have three mini in-class talks (a proposal, a progress report, and a final demo) for each project. The final project submission (via the course dropbox) should include a polished write-up (think, a short workshop paper) and the slides from your demo. Final submissions are due at 11:00 pm on March 13, 2015.

Grading

Grades will be based on the course project (50%), paper presentations (40%), and class participation (10%).

Schedule

Design space of synthesis and verification tools
Jan 06 Introduction (Emina)
Jan 09 Dimensions in synthesis and verification (Emina) [Gulwani, PPDP'10]
Jan 13 Project proposal talks
Synthesis of loop-free programs from functional specifications
Jan 16 Syntax-guided synthesis (Calvin) [Alur et al., Marktoberdorf'14]
Jan 20 Oracle-guided component-based synthesis (Alex) [Jha et al., ICSE'10]
Jan 23 Synthesis via smart sampling (James W) [Godefroid and Taly, PLDI'12]
Jan 27 Stochastic synthesis (John) [Schkufza et al., ASPLOS'13]
Verification and synthesis of imperative, functional, and concurrent programs
Jan 30 Template-based verification and synthesis of imperative programs (James B) [Srivastava et al., STTT'12]
Feb 03 Verification and synthesis of recursive functional programs over unbounded domains (Konstantin) [Kneuss et al., OOPSLA'13]
Feb 06 Verification and synthesis with a Haskell-based solver-aided host language (Adriana) [Uhler and Dave, OOPSLA'14]
Feb 10 Abstraction-guided synthesis of synchronization in concurrent programs (Doug) [Vechev et al., POPL'10]
Feb 13 Project development talks
Verification and synthesis of low-level programs
Feb 17 Deductive synthesis of linear DSP transforms (Pavel) [Puschel et al., PGOA'05]
Feb 20 User-guided reactive synthesis of device drivers (James W) [Ryzhyk et al., OSDI'14]
Feb 24 Verification via testing and abstraction (Adriana) [Beckman et al., ISSTA'08]
Feb 27 Verification via exhaustive testing (James B) [Christakis and Godefroid, VMCAI'15]
Synthesis of high-level programs from multi-modal specifications
Mar 03 Synthesis with version space algebra (Calvin) [Lau et al., ML'03]
Mar 06 Synthesis via crowd sourcing (Alex) [Cochran et al., POPL'15]
Mar 10 Dynamic synthesis for code completion (Konstantin) [Galenson et al., ICSE'14]
Mar 13 Project presentations and demos