• 20. 2. 2014: Cancelled

• 27. 2. 2014: Introduction, Relation to Other Courses, Basic Taxonomy of Formal Verification Techniques

• 6. 3. 2014: Deductive Software Verification, Partial and Complete Correctness, Verification of Flowcharts, Axiomatic Program Verification

• 13. 3. 2014: Model Checking: An Overview

• 20. 3. 2014: Reachability in Pushdown Systems

• 27. 3. 2014: Abstraction and CEGAR
• 3. 4. 2014: Abstraction and CEGAR (cont.)

• 10. 4. 2014: Symbolic Execution (Marek Trtík)

• 17. 4. 2014: Abstract Interpretation + Static Analysis
• 24. 4. 2014: Cancelled

• 15. 5. 2014 - Theorem prover ACL2. [handout: acl2_handout.pdf] [demonstration: script.acl2] [application of HOL Light: Flyspeck] [demonstration of Dafny@rise4fun]

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