- 교수 Instructor: 허기홍 Kihong Heo ([email protected])
- 조교 TAs (mailing list: [email protected])
- 장수진 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
본 강의의 핵심 주제는 안전하고 믿을만한 소프트웨어를 만들기 위한 "명세와 구현 사이의 관계"입니다. 크게 아래와 같은 두 가지 세부 주제를 다룹니다:
- 프로그램 검증 (program verification): 주어진 구현이 해당 명세를 만족하는지 어떻게 자동으로 증명할 것인가?
- 프로그램 합성 (program synthesis): 주어진 명세를 만족하는 구현을 어떻게 자동으로 만들어낼 것인가?
학생들은 강의와 숙제를 통해 프로그램 검증과 합성의 이론과 실제를 배울 것입니다.
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 is for students who actively participate and express what they have learned in a diverse way.
- 매 수업시간에 항상 여러분을 만날 수 있기를 기대합니다. 출석은 정량평가하지 않습니다. 정량화 할 만큼 가치가 낮지 않기 때문입니다.
- I always look forward to seeing you in every class. Attendance is not quantitatively assessed because it is too valuable to be reduced to a mere number.
- 적극적인 참여로 본인이 배운 바를 스스로 다채롭게 내뿜는 학생들을 위한 보상입니다.
이 강의는 P/NR 성적을 허용하지 않습니다. 신입생은 반드시 교수에게 이메일을 통해 사전 승인을 받은 후 수강신청하길 바랍니다.
This course DOES NOT allow for P/NR grading. Freshmen can enroll in this course only if they have prior approval from the instructor. Send an email to the instructor for approval.
- 강의자료가 제공됩니다. Lecture slides will be provided.
- Program Synthesis (PS)
- Introduction to Program Synthesis (IPS)
- The Calculus of Computation (COC)
이 강의에서 학생들은 다양한 프로그래밍 숙제를 통해 프로그램 검증기와 합성기를 설계하고 구현하는 법을 배웁니다. 특히 여기에 있는 몇 가지 도구를 사용할 예정입니다.
프로그램 검증기 채점을 위한 프로그램은 BugSynth를 이용하여 자동으로 생성됩니다. BugSynth는 LLM과 프로그램 검증 기술을 활용하여 자연스럽고 믿을만한 채점용 오류 프로그램을 생성하는 도구입니다.
모든 숙제 제출은 Github와 Gradescope 를 통해서 이루어집니다. 매 숙제마다 제출을 위한 GitHub Classroom 초대 URL이 게시판에 공지됩니다. 초대를 수락하면, 여러분의 숙제를 위한 비공개 개인 저장소가 만들어 질 것입니다. 여러분은 제출 기한 이전에 원하는 만큼 해당 저장소에 제출할 수 있고, 이 저장소를 Gradescope에 제출하여 채점결과를 확인할 수 있습니다.
기한을 넘겨서 제출할 시 아래와 같은 규정에 따라 채점합니다:
- 하루 늦을 시 점수의 80%
- 이틀 늦을 시 점수의 50%
- 사흘 이상 늦을 시 0%
This course includes programming assignments through which students will learn how to design and implement program verifiers and program synthesizers. Students will use a few tools described here.
The program for grading program verifiers is automatically generated using BugSynth. BugSynth utilizes LLM and program verification techniques to generate natural and reliable buggy programs for grading.
All submissions will be managed using GitHub and Gradescope. 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. You can submit this repository to Gradescope to check your grading results.
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
학문 윤리를 어긴 수강생은 F를 받습니다. 자세한 사항은 KAIST 전산학부 명예규정을 참고하십시오.
세상에 널린 자료 (예: 구글 검색, ChatGPT)를 참고하는 것은 좋지만, 그대로 베끼는 것은 윤리에 어긋납니다. 제출한 과제는 기존 저작물(다른 수강생, 과거 수강생, AI 생성물 등)과 자동으로 비교하여 표절물을 검사합니다. 완전히 본인의 것으로 재창조하지 않고 기존 저작물과 비슷한 경우는 표절로 판단합니다. 이러한 원칙은 AI도구가 등장했다고 해서 달라지지 않습니다.
Students who violate academic integrity will get an F. See the KAIST CS honor code.
It’s fine to refer to readily available resources (e.g., Google searches, ChatGPT), but copying them directly is unethical. Submitted assignments will be automatically compared to existing works (other students’ work, past students’ work, AI-generated content, etc.) to check for plagiarism. If the work closely resembles existing material without being fully recreated as your own, it will be considered plagiarism. This principle remains unchanged even in the AI era.
| 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).
- CS402: 전산논리학 개론 (Introduction to Logic for Computer Science), KAIST
- 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.
- Formal Software Verification Measures Up, CACM 2021
- Automated Reasoning @ Amazon
- Machine-assisted Proof
- Infer
- CodeQL
- Lessons from Building Static Analysis Tools at Google, CACM 2018
- Scaling Static Analysis at Facebook, CACM 2019
- Detect Bugs Early with the Static Analyzer, Apple WWDC 2021
- 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
- Autocorrect Errors in Excel, Nature 2021
- Trustworthy AI