/cs492-program-reasoning

Primary LanguagePython

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

Logistics

Course Description

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:

  1. program verification: how to automatically prove whether a given implementation satisfies the specification,
  2. 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.

Grading

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

This course does not allow for P/NR grading.

Textbook

Homework

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 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 an 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
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

Hall of Fame

Have fun with student artifacts from previous semesters here (distinguished essays, drawings, etc).

Related & Advanced Course

Acknowlegement

A large part of the slides is based on the lecture notes of similar courses:

References