|
|
COS Independent Work Seminar:
|
COS IW08
|
Do you wish sometimes that programs would just write themselves? Wouldn’t it be great if you could somehow say what a program should do, sketch a program outline, but the rest would get automatically generated? While this is difficult to do for large Java and C programs (and COS 126/217/226 programming assignments!), it is quite possible in domain-specific languages for a variety of applications. Indeed, automated synthesis of programs is an active area of research in programming languages and formal verification. Available tools aim at automatically generating programs by filling in holes in a partially-complete program sketch or by using input-output examples, optionally using grammar rules that define the underlying search space of candidate programs.
Students in the seminar will choose from a range of program synthesis domains and applications, or choose one of their own interest. Examples include automatic parallelization of array-handling programs, bit-twiddling code, spread-sheet macros, etc. They will use available synthesis tools (such as Sketch, Rosette, Prose), design their own libraries of program sketches, specify the correctness requirements, and experiment with different synthesis strategies to generate a variety of target programs. Those interested in backend techniques can also design and implement new synthesis strategies using SMT (Satisfiability Modulo Theory) solvers that perform the search and verification in these tools. Students may work on a team project, but with prior permission of the instructor, and where each student has a distinct semester-size component of the project.
There are no prerequisites for this seminar beyond COS 217 and COS 226; familiarity with functional programming or proofs of correctness (e.g., COS 326) would be useful. Students will be expected to attend all seminar meetings. The first two seminar meetings will provide background and introduction to program synthesis tools. The remaining meetings will be used for discussions on project proposals, techniques, and updates; with students reporting their progress each week and doing a class presentation at the end.
| Date | Topic | Notes and References |
| Tue Feb 2 | Introductions and Background | Background Papers: [B1] [B2] [B3] |
| Feb 9 | Background and Tools | Synthesis Tools: [T1] [T2] [T3] |
| Feb 16 | Project Ideas | Bring a draft proposal to share |
| Feb 23 | Proposal presentations | March 2 | Proposal presentations, project updates |
| Mar 9 | Progress updates, discussion, and feedback | |
| Mar 16 | Spring recess, no class | |
| Mar 23 | Status updates | |
| March 30 | Status update presentations | Draft of Introduction due |
| Apr 6 | Practice Talks w. Demos | Draft of Approach due |
| Apr 13 | Practice Talks w. Demos | Draft of Implementation due |
| April 20 | Written reports: discussion, suggestions | |
| April 27 | Last class: discussion, suggestions |