- Instructor: Sunbeom So
- Location: EECS B203
- Time: Mon/Wed 13:00-14:30
Software Engineering is an engineering discipline that is concerned with all aspects of SW production process. In particular, SW validation is highly important in the SW process due to the prevalence of SW errors, comprising more than half of the SW development cost. Our focus in this course is to study program analysis methods, which are fundamental and modern technologies that can effectively help the SW validation process.
Note1: This instruction assumes that you are using the Linux command line interface. For Windows users, I recommend using WSL.
Note2: I checked that the following commands successfully work for the clean docker image python:3.9.19-slim.
Installing OCaml
$ chmod +x setup/ocaml.sh; ./setup/ocaml.sh
Installing Z3
$ eval $(opam env); chmod +x setup/z3.sh; ./setup/z3.sh
If your installations were successful, you must get appropriate results by executing the following commands.
$ cd setup
$ eval $(opam env); chmod +x test_ocaml.sh; ./test_ocaml.sh
$ export PYTHONPATH=$home/mylib:$PYTHONPATH; python3 ex.py
| # | Date | Topics | Recommended Reading |
|---|---|---|---|
| 0 | 2/26 | Course Overview | |
| 1 | 2/28,3/4 | Introduction to Program Analysis | |
| 2 | 3/6 | Fuzzing | |
| 3 | 3/11 | Propositional Logic (1) | The Calculus of Computation Ch. 1 |
| 4 | 3/13, 3/18 | Propositional Logic (2) | The Calculus of Computation Ch. 1 |
| 5 | 3/20, 3/25 | First-Order Logic | The Calculus of Computation Ch. 2 |
| 6 | 3/27 | First-Order Theories | The Calculus of Computation Ch. 3 |
| 7 | 4/1 | Problem Solving using SMT Solvers | |
| 8 | 4/3 | Functional Programming in OCaml | |
| 9 | 4/8 | Problem Solving using SMT Solvers (2) | |
| - | 4/15 | [Mid-term Exam] | |
| - | 4/22 | [Reviewing Mid-term Exam] | |
| 10 | 4/24 | Program Verification (1) | The Calculus of Computation Ch. 5 |
| 11 | 4/29 | Program Verification (2) | The Calculus of Computation Ch. 5 |
| 12 | 5/8 | Program Verification (3) | |
| 13 | 5/13 | Program Verification (4) | Houdini Paper |
| 14 | 5/14 | Symbolic Execution | A Survey of Symbolic Execution Techniques |
| - | 5/16 | Review + Detailed Guidance about hw1 | |
| 15 | 5/27 | Symbolic Execution (2) | |
| 16 | 5/29 | Abstract Interpretation (1) | Semantics with Applications Ch. 7 |
| 17 | 5/31,6/3 | Abstract Interpretation (2) | |
| 18 | 6/5 | Abstract Interpretation (3) |
My lecture slides are based on the materials from the following courses. I am truly grateful to their authors, as these materials greatly helped improve the quality of this course.
- AAA615:Formal Methods course taught by Prof. Hakjoo Oh at Korea University
- CS398L:Automated Logical Reasoning course taught by Prof. Isil Dillig at UT Austin
- CIS547:Software Analysis course taught by Prof. Mayur Naik at UPenn