IA159 Formal Verification Methods
Programme & slides
- 22. 2. 2018: Introduction, Relation to Other Courses, Basic Taxonomy of Formal Verification Techniques, Topics of This Course
- 1. 3. 2018: Theorem Prover ACL2 [handout: acl2_handout.pdf] [demonstration: script.acl2] [application of HOL Light: Flyspeck] [demonstration of Dafny@rise4fun, Example1, Example2, Challenge1, Challenge2] (This lecture will not be the subject of final examination.)
- 8. 3. 2018: Reachability in Pushdown Systems
- 15. 3. 2018: LTL Model Checking of Pushdown Systems (This lecture will not be the subject of final examination.)
- 22. 3. 2018: Translation of LTL to Büchi Automata via Alternating Automata
- 29. 3. 2018: Partial Order Reduction - part I
- 5. 4. 2018: Partial Order Reduction - part II
- 12. 4. 2018: Abstraction - part I
- 19. 4. 2018: Cancelled
- 26. 4. 2018: Abstraction - part II
- 3. 5. 2018: Static Analysis and Abstract Interpretation
- 10. 5. 2018: Shape Analysis via 3-Valued Logic [(semi)demo: TVLA output without bug and with bug]
- 17. 5. 2018: Verification via Automata, Symbolic Execution, and Interpolation [used in Ultimate Automizer]
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2018/IA159/um/notes.pdf
Následující