IA159 Formal Verification Methods
Programme & slides
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/01_intro.pdf
- 22. 2. 2017: Introduction, Relation to Other Courses, Basic Taxonomy of Formal Verification Techniques, Topics of This Course
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/02_acl2.pdf
- 1. 3. 2017: 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.)
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/03_pda.pdf
- 8. 3. 2017: Reachability in Pushdown Systems
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/04_ltl2ba.pdf
- 15. 3. 2017: Translation of LTL to Büchi Automata via Alternating Automata (presented by Fanda Blahoudek)
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/05_por.pdf
- 22. 3. 2017: Partial Order Reduction - part I
- 29. 3. 2017: Partial Order Reduction - part II
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/06_abs.pdf
- 5. 4. 2017: Abstraction - part I
- 12. 4. 2017: Abstraction - part II
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/07_absint.pdf
- 19. 4. 2017: Static Analysis and Abstract Interpretation
- 26. 4. 2017: Cancelled
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/08_shape.pdf
- 3. 5. 2017: Shape Analysis via 3-Valued Logic [(semi)demo: TVLA output without bug and with bug]
- 10. 5. 2017: Cancelled (Dies Academicus)
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2017/IA159/um/09_ultimate.pdf
- 17. 5. 2017: 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/jaro2017/IA159/um/notes.pdf
Následující