Ras Bodik and Emina Torlak Fall 2012, 310 Soda Hall, TT 11-12:30 Office hours (Ras): Wed 1-2pm, Fri 4-5pm, 565 Soda Hall (in Par Lab)Course syllabus
mailing list:cs294-synthesis google group
Topics: What is program synthesis? How to perform synthesis with constraint solvers? Constraint solver as a program evaluator and program execution inverter. Why synthesis now? Synthesis vs. compilation. Example of real-world synthesizers. What artifacts might be synthesizable? Introduction to course format and overview of course project.
Topics: Four programming problems solvable when a program is translated into a logical constraint: verification, fault-localization, synthesis, and angelic programming. Constructing the formulas for these problems given an encoding of a program. Example of a simple SMT program encoding. Demonstrating the four problems on the Z3 solver.
Topics: Encoding of arrays. Single assignment form. Integer and bitvector encodings logics. Extensional theory of arrays. First introduction to the Racket language: a simple formula generator with quotes and unquotes. Ideas for the semester project.
Assigned reading (due next lecture): Encoding for loops and other good stuff. D. Kroening, E. Clarke and K. Yorav, Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking, DAC 2003.
Topics: Guest lecture by Niklas Een, co-designer of MiniSAT. Algorithms of modern (CDCL) SAT solvers: implication view of CNF, decision heuristics, propagation techniques, conflict analysis. Encoding problems in CNF: Slither Link, incremental encoding. MiniSAT API. Bounded model checking.
Topics: Relational logic. Encoding loops. Modeling the heap, including updates to object fields. Static assignment for the heap. Partial models. Verification, bug localization, and synthesis with relational formulas. Tutorial on the Kodkod solver.
Topics: Increase the level of programming abstraction. Language properties desired in general and for synthesis in particular. Examples of small languages (geometry construction, relational data structures, automata protocols).
Assigned reading (due next lecture): Implementing languages in Racket. Danny Yoo, Fudging up a Racket.
Topics: Students present their project proposals. Problem statement. What is the specification.
Files: Student presentations Date: September 13, 2012
Topics: Implementing languages in Racket. Syntactic abstraction with macros.
Date: September 18, 2012
Read before the lecture (optional): Creating Languages in Racket (Sometimes you just have to make a better mousetrap), by Matthew Flatt.
Slides: screencast Date: September 20, 2012
Date: September 25, 2012
Topics: You will synthesize programs in this language.
Topics: Lifting built-in operators to the symbolic domain. Partial evaluation. Bounded unwinding. Discussion of challenges translating assertions, in the context of assertions for guarding bounded unwinding.
Slides: screencast Date: October 02, 2012
Topics: Guest Lecture by Sumit Gulwani.
Topics: Translation of recursive programs. Discussion of translating imperative programs guided by the translation of the brainfudge interpreter to formulas.
Topics: You will study programs in your domain and define holes. In your presentation, you will show sketches in your language and show a demo of running programs (this demo does not include hols).
Topics: Solving synthesis problems with sim-syn. Overflow in bitvector encodings. Sketching expressions. Bottom-up versus top-down construction of path conditions. Making vector operations symbolic. Translating side-effect functions to logic.
Slides: screencast Date: October 16, 2012
Date: October 18, 2012
Read before the lecture (optional): Learning Programs from Traces using Version Space Algebra
Date: October 23, 2012
Date: October 25, 2012
Emina Torlak and I have given an invited tutorial at CAV 2012. The tutorial is being expanded this semester into a graduate course, which you can follow as we add lectures and homeworks. CAV tutorial slides: (ppt, pdf, screencast). The graduate course.8/13/2012
We are looking for postdocs in synthetic biology. We need curious, well-rounded computer scientists with expertise in algorithms, hacking, and with interest in biology.4/3/2012
The multi-university ExCAPE project aims to change computer programming from the tedious task to one in which a programmer and an "automated program synthesis tool" collaborate to generate software that meets its specifications.4/3/2012
We are looking for postdocs in program synthesis and computer-aided programming.4/9/2012
Several communities related to synthesis of programs and other computational artifacts will meet again in wine cellars of the castle.