Formal Methods, 2017 Fall
Course Information
- Instructor: Hakjoo Oh
- Lecture: 09:00-11:30 on Mondays
- Textbook:
Slides
- Overview: lec0.pdf
- Propositional Logic: lec1.pdf
- First-Order Logic: lec2.pdf
- First-Order Theories: lec3.pdf, lec4.pdf
- Program Verification: lec5.pdf
- Program Analysis: lec6.pdf, lec7.pdf, lec8.pdf
- Symbolic Execution: lec9.pdf
Homework
- HW1 (due 10/30, in class): hw1.pdf
Reading
- Z3 SMT Solver
- Introductory Articles
- Research Papers
- A static analyzer for large safety-critical software
- The Octagon Abstract Domain
- Scalable error detection using boolean satisfiability
- Combinatorial sketching for finite programs
- Synthesis of loop-free programs
- Oracle-guided component-based program synthesis
- Cause clue clauses: error localization using maximum satisfiability
- Automated Whitebox Fuzz Testing
Software Analysis Lab. @ Korea University