CSE4051
CSE4051 Program Verification
News
Basic Information
- Instructor: Woosuk Lee
- Office Location: Rm#403, Eng. Bldg 3
- Telephone: 031-400-1031
- Email: woosuk at hanyang.ac.kr
- Office Hours: Monday 14:00 - 16:00
- Time & Location
- Monday and Wednesday 09:00 - 10:15 @ Rm 106, 4th Eng Bldg.
- TA
- Jehyung Lee (astean1001 at gmail.com)
- Jeonghun Lee (jeonghuni443 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 |
Grading
- Homework: 16%
- Late submissions will get penalty points (-20%)
- Mid exam: 37%
- Final exam: 37%
- Attendance: 10%
Homework
- Please register for the submission system before submissions.
- Submission system
- Assignments