COSE419-24S - SAL@KU

Software Verification, 2024 Spring

Instructors

Lecturer: Hakjoo Oh
TAs: Jisuk Byun, Donguk Kim

Lectures

Part 0: Overview

Course Overview
- Slides: lec0.pdf
Introduction to Software Analysis
- Slides: lec1.pdf
- Video: (1) (2)

Part 1: Testing

Greybox Fuzzing
- Slides: lec2.pdf
- Code: greybox.py
- Video: (1) (2)
Concolic Testing
- Slides: lec3.pdf
- Video: (1)

Part 2: Verification

Propositional Logic
- Slides: lec4.pdf
- Video: (1) (2) (3)
Problem Solving using SMT Solver
- Slides lec5.pdf
- Video: (1) (2) (3)
First-order Logic
- Slides: lec6.pdf
- Video: (1) (2)
First-order Theories
- Slides: lec7.pdf
- Video: (1) (2)
Program Specification
- Slides: lec8.pdf
- Video: (1) (2)
Partial Correctness Proof
- Slides: lec9.pdf
- Video: (1) (2)
Total Correctness Proof
- Slides: lec10.pdf
- Video: (1)

Part 3: Static Analysis

Static Analysis Overview
- Slides lec11.pdf
- Video: (1) (2)
Interval Analysis
- Slides lec12.pdf
- Video: (1) (2)
Relational Analysis
- Slides lec13.pdf
- Video: (1)
Pointer Analysis
- Slides lec14.pdf
- Video: (1) (2)

Assignments

Repository
HW1: SAT Solver hw1.pdf template (due 4/5 23:59)
HW2: Problem Solving using SMT Solver (1) hw2.pdf template (due 4/19 23:59)
HW3: Problem Solving using SMT Solver (2) hw3.pdf template (due 5/10 23:59)
HW4: Program Verification hw4.pdf template (due 5/30 23:59)
HW5: Static Analysis hw5.pdf template (due 6/12 23:59)

Software Analysis Lab. @ Korea University