- Instructor: Kihong Heo (허기홍, kihong.heo@prosys.kaist.ac.kr)
- TAs (mailing list: cs424.ta@prosys.kaist.ac.kr)
- Sujin Jang (장수진)
- Changgong Lee (이창공)
- Time: Mon/Wed 09:00 - 10:15
- Office hours (by appointment):
- Instructor: Mon 10:15 - 11:00
- TAs: Mon 10:15 - 11:00
- Location: N1 102
The main theme of this course is "the relationship between specification and implementation" for safe and reliable software. This course will cover two topics under the theme:
- program verification: how to automatically prove whether a given implementation satisfies the specification,
- program synthesis: how to automatically generate an implementation 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%
- This course DO NOT allow for P/NR grading.
- Freshmen can enroll in this course only if they have prior approval by the instructor. Send an email to the instructor for the approval.
- 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 synthesizers and program verifiers. 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 discussion 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 an 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, Curry-Howard Correspondence |
|
| 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 |
|
| 16 | Program Synthesis as AI | Trustworthy AI | |
| - | Final Exam |
Have fun with student artifacts from previous semesters here (distinguished essays, drawings, etc).
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.
- PL Wiki
- Search-based Program Synthesis, CACM 2018
- AI Can Write Code Like Humans—Bugs and All. Wired 2021
- Coding Made AI—Now, How Will AI Unmake Coding?, IEEE Spectrum 2022
- Neurosymbolic AI, CACM 2022
- Formal Software Verification Measures Up, CACM 2021
- Trustworthy AI
- Automated Reasoning @ Amazon
