- Instructor: Kihong Heo (kihong.heo@kaist.ac.kr)
- TAs (mailing list: is593.ta@prosys.kr)
- Hyunsu Kim (hyunsu.kim00@kaist.ac.kr)
- Seungwan Kwon (seungwan.kwon@kaist.ac.kr)
- Time: Tue/Thr 09:00 - 10:15
- Office hour: Tue 10:15 - 11:00 (by appointment)
- Location: N5 2243
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, assignments, and term projects. This course will be highly interactive and involve a significant amount of academic communication including reading, writing, and presentations.
- Assignments: 20%
- Midterm project: 30%
- Final project: 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
- Each student is required to give 4 presentations (midterm project, final project proposal, final project result, and paper presentation).
- Each student is required to give at least 1 question for each student presentation.
- Midterm project: each student will design and implement an advanced program synthesizer.
- Presentation: students will present their own idea to advance a naive program synthesizer.
- Final project: each student will define and solve your own problem related to program synthesis or program verification.
- Proposal writing: students will submit their project proposal that will be reviewed by other students, TAs, and instructors.
- Proposal presentation: students will present their plans for the project and rebut criticism from reviewers.
- Final presentation: students will present their results.
Students who violate academic integrity will get F. See the KAIST CS honor code.
| Week | Topics | Reading | Homework |
|---|---|---|---|
| 0 | Functional Programming in OCaml | ||
| 1 | Introduction | HW0: OCaml Programming | |
| Introduction to Program Synthesis | PS Ch1-2, IPS Lec1 | HW1: Reading Critique | |
| 2 | Inductive Synthesis and Enumerative Search | PS Ch4.1, IPS Lec2-4 | |
| Search Space Pruning | |||
| 3 | Search Space Prioritization | HW2: Reading Critique | |
| Representation-based Search | HW3: Program Synthesizer | ||
| 4 | Program Synthesis and Verification | ||
| Introduction to Program Verification | |||
| Propositional Logic | COC Ch1 | ||
| 5 | First-order Logic | COC Ch2 | |
| First-order Theory | COC Ch3 | ||
| 6 | Hoare Logic | COC Ch5 | HW4: Reading Critique |
| 7 | Automatic Verification using Contrained Horn Clauses | HW5: Program Verifier | |
| Midterm Project Presentation (1) | |||
| 8 | Midterm Project Presentation (2) | ||
| No class (midterm week) | |||
| 9 | Midterm Project Presentation (3) | ||
| Midterm Project Presentation (4) | HW6: Final Project Proposal | ||
| 10 | Proposal Review & Discussion | ||
| No class (Children's day) | |||
| 11 | No class (ICSE) | ||
| Paper Presentation (1) | |||
| 12 | Paper Presentation (2) | ||
| No class (Graduate admission) | |||
| 13 | Paper Presentation (3) | ||
| Paper Presentation (4) | |||
| 14 | Final Project Presentation (1) | ||
| Final Project Presentation (2) | HW7: Reading Critique | ||
| 15 | Final Project Presentation (3) | ||
| Final Project Presentation (4) | |||
| 16 | Final Project Presentation (5) |
- DPGen: Automated Program Synthesis for Differential Privacy, CCS'21
- Syntia: Synthesizing the Semantics of Obfuscated Code, USENIXSEC'17
- Data-Driven Synthesis of Provably Sound Side Channel Analyses, ICSE'21
- An Inductive Synthesis Framework for Verifiable Reinforcement Learning, PLDI'19
- Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Term Rewriting, PLDI'20
- Synthesizing Highly Expressive SQL Queries from Input-Output Examples, PLDI'17
- Combinatorial sketching for finite programs, ASPLOS'06
- Synthesis of Data Completion Scripts using Finite Tree Automata, OOPSLA'17
- Verifying Correct Usage of Context-Free API Protocols, POPL'19
- Verified Three-Way Program Merge, OOPSLA'18
- Alive2: bounded translation validation for LLVM, PLDI'21
- Reluplex: An efficient SMT solver for verifying deep neural networks, CAV'17
- Formally Verified Mathematics, CACM'14
- Verifying Constant-Time Implementations, USENIXSEC'16
- Towards a Verified Range Analysis for JavaScript JITs, PLDI'20
- VERISMART: A Highly Precise Safety Verifier for Ethereum Smart Contracts, SNP'20
A large part of the slides is based on the lecture notes of similar courses by