Skip to content

kingdoctor123/cs492-program-reasoning

 
 

Repository files navigation

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

Logistics

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:

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

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

Hall of Fame

Have fun reading the distinguished essays from previous semesters here.

Advanced Course

Acknowlegement

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

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published