• 19. 2. 2015: Introduction, Relation to Other Courses, Basic Taxonomy of Formal Verification Techniques
• 26. 2. 2015: Cancelled

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

• 12. 3. 2015: Theorem Prover ACL2. [handout: acl2_handout.pdf] [demonstration: script.acl2] [application of HOL Light: Flyspeck] [demonstration of Dafny@rise4fun, Example1, Example2, Challenge1, Challenge2] (not required for the examination)

• 19. 3. 2015: Model Checking: An Overview

• 26. 3. 2015: Reachability in Pushdown Systems
• 2. 4. 2015: LTL Model Checking of Pushdown Systems

• 9. 4. 2015: Abstraction - part I
• 16. 4. 2015: Cancelled
• 23. 4. 2015: Abstraction - part II

• 30. 4. 2015: Symbolic Execution

• 7. 5. 2015: Abstract Interpretation + Static Analysis
• 14. 5. 2015: ic3 (no slides, not required for the examination)

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