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

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)

Software Analysis Lab. @ Korea University