- Instructor: Kihong Heo (kihong.heo@kaist.ac.kr)
- TAs (mailing list: cs492.ta@prosys.kr)
- Time: Tue/Thu 09:00 - 10:15
- Office hour (by appointment):
- Instructor: Tue 10:15 - 11:00
- TAs: Fri 15:00 - 16:00
- Location: E3 2111
The main theme of this course is "the relationship between specification and program" for safe and reliable software. This course will cover two topics under the theme:
- program verification: how to automatically prove whether a given program satisfies the specification,
- program synthesis: how to automatically generate a program that satisfies the specification.
Students will learn theories and practices of program verification and synthesis through lectures, and assignments.
- Homework: 50%
- Final Exam: 40%
- Participation: 10%
- Lecture slides will be provided
- Program Synthesis (PS)
- Introduction to Program Synthesis (IPS)
- The Calculus of Computation (COC)
This course includes programming assignments through which students will learn how to design and implement program synthesizer and program verifier. Students will use a few tools which are described here.
All submissions will be managed using Github.
For each assignment, a unique invitation URL for Github Classroom will be posted in the issue board.
Once you accept the invitation, a private repository for your assignment will be created.
You can push as many commits as you want before the deadline. We will grade the final commit of your master branch.
The late homework policy is as follows:
- 80% credit for one day late
- 50% credit for two days late
- NO credit given after two days late
Students who violate academic integrity will get F. See the KAIST CS honor code.
| Week | Topics | Reading | Homework |
|---|---|---|---|
| 0 | Functional Programming in OCaml |  HW0: Hello-world, OCaml Programming |
|
| 1 | Introduction |  Undecidability   |
|
| 2 | Operational Semantics | HW1: SmaLLVM Interpreter |
|
| 3 | Concepts in Program Verification | ||
| 4 | Propositional Logic | COC Ch1 | |
| 5 | First-order Logic | COC Ch2 | |
| 6 | First-order Theory | COC Ch3 | HW2: Automated Theorem Proving |
| 7 | Hoare Logic | COC Ch5, CACM'21 | |
| 8 | Automated Program Verification | HW3: SmaLLVM Verifier |
|
| 9 | Overview of Program Synthesis | PS Ch1-2, IPS Lec1, Wired, IEEE Spectrum, CACM | |
| 10 | Inductive Synthesis and Enumerative Search | PS Ch4.1, IPS Lec2-4 | HW4: LIA Synthesizer |
| 11 | Search Space Pruning | ||
| 12 | Search Space Prioritization | CACM'18 | |
| 13 | Representation-based Search | HW5: SLIA Synthesizer |
|
| 14 | Constraint-based Search | ||
| 15 | Functional Synthesis | HW6: CEGIS |
|
| - | Final Exam |
Have fun reading the distinguished essays from previous semesters here.
- CS524: Program Analysis, KAIST
A large part of the slides is based on the lecture notes of similar courses:
- CS389: Automated Logical Reasoning, Univ. of Texas at Austin
- AAA528: Computational Logic, Korea Univ.
- CSE291: Program Synthesis, UCSD
- CSE9116: Program Synthesis, Hanyang Univ.