IA159 Formal Verification Methods

Programme & slides

  1. 25. 2. 2010: Introduction, relation to other courses, basic taxonomy of formal verification techniques. [slides: 01_intro.pdf]
  2. 4. 3. 2010: Formal aspects of software testing, coverage criteria, model-based testing. [slides: 02_testing.pdf] Bonus: Automated whitebox fuzz testing.
  3. 11. 3. 2010: Deductive software verification, partial and complete correctness, verification of flowcharts, axiomatic program verification. [slides: 03_deductive.pdf]
  4. 18. 3. 2010: Deductive software verification (cont.). Theorem prover ACL2. [slides: 04_acl2.pdf] [handout: acl2_handout.pdf] [demonstration: script.acl2]
  5. 25. 3. 2010: cancelled
  6. 1. 4. 2010: Theorem prover ACL2 (cont.). 
  7. 8. 4. 2010: Model checking: an overview. [slides: 05_mc.pdf]
  8. 15. 4. 2010: LTL to BA via alternating 1-weak BA. [slides: 06_ltl2ba.pdf]
  9. 22. 4. 2010: Partial order reduction. [slides: 07_por.pdf]
  10. 29. 4. 2010: Partial order reduction (cont.). LTL model checking of pushdown systems. [slides: 08_pda.pdf]
  11. 6. 5. 2010: LTL model checking of pushdown systems (cont).
  12. 13. 5. 2010: Abstraction and CEGAR. [slides: 09_abs.pdf]
  13. 20. 5. 2010: Abstraction and CEGAR (cont).
The current version of lecture notes
updated on 18.4.2010
Předchozí
Následující