Course Information
- Speaker: Prof. Willem Visser
- Affiliation: Computer Science, Stellenbosch University, South Africa
- Time: 2014.11.24(Mon)~ 11.29(Fri), PM 2:00~5:00
- Location: Oh Sang-Su Seminar Room (E3-1, #4443)
- Host: 김문주 교수 (T. 3543)
Syllabus
Monday (Nov 24, 2014) - Model Checking (Slides)
- Brief History of Model Checking
- The Models of Model Checking (Paper)
- Temporal Logic (linear vs branching) (Property Patterns Paper)
- Model Checking Algorithms (explicit, symbolic and bounded)
Tuesday (Nov 25, 2014) - Software Model Checking (Slides)
- Hardware vs Software Model Checking
- Early days of Software Model Checking
-
Software Model Checking
- CBMC
- ESBMC
- Java PathFinder
- Other types of model checking (e.g. timed, probabilistic, statistical) (Survey of Statistical Model Checking)
Wednesday (Nov 26, 2014) - Symbolic Execution (Slides1, Slides2, Slides3)
- Background
- Symbolic Pathfinder (SPF)
- Classic vs Concolic
- SAT and SMT
Thursday (Nov 27, 2014) - Advanced Symbolic Execution (Slides)
- Green
- Model Counting
- Probabilistic Symbolic Execution
- New research directions
Friday (Nov 28, 2014) - New Ideas (Slides), Static Analysis (Slides) and Conclusions (Slides)
- Test Coverage, Ranking Program Correctness and Analyzing Mutations
- Path sensitive vs insensitive analysis (bug finding vs correctness)
- Pattern based analyses
- Static Analysis for bug finding and testing
- Conclusions