• 21. 2. 2012: Introduction, relation to other courses, basic taxonomy of formal verification techniques.

• 28. 2. 2012: Deductive software verification, partial and complete correctness, verification of flowcharts, axiomatic program verification.

• 6. 3. 2012: Theorem prover ACL2. [handout: acl2_handout.pdf] [demonstration: script.acl2] [application of HOL Light: Flyspeck]

• 13. 3. 2012: Model checking: an overview

• 20. 3. 2012: Reachability in Pushdown Systems
• 27. 3. 2012: cancelled
• 3. 4. 2012: LTL Model Checking of Pushdown Systems

• 10. 4. 2012: Abstraction and CEGAR
• 17. 4. 2012: Abstraction and CEGAR (cont.)

• 24. 4. 2012: Symbolic Execution

• 15. 5. 2012: Abstract Interpretation + Static Analysis

There is one important topic not covered by the course (and exam), namely "runtime verificaion".