CS492: Program Reasoning (프로그램 논증)

Logistics

Instructor: Kihong Heo (kihong.heo@kaist.ac.kr)
TAs (mailing list: cs492.ta@prosys.kr)
- Seungwan Kwon (seungwan.kwon@kaist.ac.kr)
- Sujin Jang (sujin0529@kaist.ac.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

Course Description

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.

Grading

Homework: 50%
Final Exam: 40%
Participation: 10%

Textbook

Lecture slides will be provided
Program Synthesis (PS)
Introduction to Program Synthesis (IPS)
The Calculus of Computation (COC)

Homework

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

Academic Integrity Violation

Students who violate academic integrity will get F. See the KAIST CS honor code.

Schedule

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		HW5: SLIA Synthesizer
12	Search Space Prioritization	CACM'18
13	Representation-based Search
14	Program Synthesis and Verification		HW6: CEGIS
15	Wrap Up
16	No class