CSE4051
CSE4051 Program Verification
News
Basic Information
- Instructor: Woosuk Lee
- Office Location: Rm#410, Hakyeonsan Cluster Building
- Telephone: 031-400-1031
- Email: woosuk at hanyang.ac.kr
- Office Hours: Thursday 14:00 - 16:00
- Time & Location
- Wednesday and Thursday 10:30 - 11:45 @ Rm 405, Multidisciplinary Lecture Hall
- TA
- Gangdae Ju (jugangdae at gmail.com)
References
- Calculus of Computation (CoC)
- Decision Procedure (DP)
- E-books of CoC and DP are available at lib.hanyang.ac.kr
- Self-contained slides and source codes will be provided.
Slides
| Topic | Slides | Reference |
|---|---|---|
| Course overview | lec1 | |
| Propositional Logic | lec2 | CoC 1.1-1.5 |
| Applications of SAT | lec3 | Notebook |
| CDCL Algorithm | lec4 | DP 2.2 |
| First-Order Logic | lec5 | CoC 2.1-2.5 |
| First-Order Theories | lec6 | CoC 3.1-3.7 |
| Applications of SMT | lec7 | Notebook |
| Theory Solvers | lec8 | CoC 9.1-9.2 |
| Combining Theories | lec9 | CoC 10 |
| DPLL(T) | lec10 | DP 3 |
| Program Specification | lec11 | CoC 5 |
| Partial Correctness | lec12 | CoC 5,6 |
| Intro to Dafny | lec13 | |
| Total Correctness | lec14 | CoC 5,6 |
| Intro to Lean | lec15 |
Grading
- Homework: 10%
- Late submissions will get penalty points (-20%)
- Mid exam: 40%
- Final exam: 40%
- Attendance: 10%
Homework
- Please register for the submission system before submissions.
- Submission system
- Assignments