IA159 Formal Verification Methods

Programme & slides

  1. 19. 2. 2009: Introduction, relation to other courses, basic taxonomy of formal verification techniques.
  2. 26. 2. 2009: Formal aspects of software testing, coverage criteria, model-based testing. [slides: 02_testing.pdf]
  3. 5. 3. 2009: Deductive software verification, partial and complete correctness, verification of flowcharts, axiomatic program verification. [slides: 03_deductive.pdf]
  4. 12. 3. 2009: Deductive software verification (cont.). Theorem prover ACL2. [slides: 04_acl2.pdf] [handout: acl2_handout.pdf] [demonstration: script.acl2]
  5. 19. 3. 2009: Theorem provever ACL2 (cont.) + demonstration. Model checking: quick overview. [slides: 05_mc.pdf]
  6. 26. 3. 2009: LTL -> BA via alternating 1-weak BA. [slides: 06_ltl2ba.pdf]
  7. 2. 4. 2009: cancelled
  8. 9. 4. 2009: Partial order reduction. [slides: 07_por.pdf]
  9. 16. 4. 2009: cancelled
  10. 23. 4. 2009: Partial order reduction: part II. [slides: 07_por.pdf]
  11. 30. 4. 2009: Model checking of infinite-state systems. LTL model checking of pushdown systems. [slides: 08_pda.pdf]
  12. 7. 5. 2009: LTL model checking of pushdown systems (cont.). [slides: 08_pda.pdf]
  13. 14. 5. 2009: Abstraction and CEGAR. [slides: 09_abs.pdf]
  14. 21. 5. 2009: Abstraction and CEGAR (cont.). [slides: 09_abs.pdf]
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2009/IA159/um/notes.pdf
Předchozí
Následující