Program Synthesis (Fall 2016)

ECEN 5033, CSCI 7000-002

Instructor Pavol Cerny
Lectures Mon, Wed 3-4.15 in ECEE 265
Office hours Wed 4.15-5.15pm in ECEE 120, and by appointment

Course description

Computer-aided programming, or partial-program synthesis, is emerging as an effective approach for increasing programmer productivity. Its goal is to harness the improvements in constraint-solving technology and the increase in routinely available computational power in order to enable programmers to express insights in a variety of forms such as incomplete programs, example behaviors, and high-level requirements. In the course, we will cover the foundations, as well as current research and prototype tools.

Course topics

What can you expect to get out of the course:
  • Learn about program synthesis algorithms:
    • Enumerative synthesis
    • Counter-example guided synthesis
    • Proof-based synthesis
    • Synthesis with version-space algebra
    • Type-based synthesis
    • Classical search algorithms and machine learning
    • Solver-aided languages
    • Automata-based synthesis and graph games
    • Quantitative synthesis
    • Deductive synthesis
  • Learn about technical topics useful in synthesis, verification, program analysis; as needed:
    • specification logics
    • encoding programs as logical formulas
    • constraint solving (SAT, SMT)
    • (bounded) model checking
    • abstract interpretation
  • Practical experience with computer-aided programming tools

Advertisement/warning: This is a class on a very recent research topic. Expect to read research papers.

Schedule

Synthesis algorithms


Course project

The goal of your project is to build a synthesizer for a domain of your choice (ideally, related to your research interests). Project deadlines:
  • September 26: project proposal; 2 page report
  • November 2: checkpoint (project works on motivating examples; submit source code, examples; 4 page report)
  • December 2: project submission deadline (submit source code, examples, 6 page report)
  • December 5,7: project presentations, demos

Relevant links

  • LNCS 2500 : Automata, Logics, and Infinite Games: A Guide to Current Research
  • Recent large research project on synthesis.

Grading

The course will be graded based on a course project(40% of the course grade), in class presentations (30%), paper summaries (20%) and class participation (10%).

Syllabus statement

A statement of class policies is available here.