IA159 Formal Verification Methods
Programme & slides
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/01_intro.pdf
- 24. 2. 2016: Introduction, Relation to Other Courses, Basic Taxonomy of Formal Verification Techniques
- 2. 3. 2016: Cancelled
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/02_acl2.pdf
- 9. 3. 2016: 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)
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/03_pda.pdf
- 16. 3. 2016: Reachability in Pushdown Systems
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/04_ltl2ba.pdf
- 23. 3. 2016: Translation of LTL to Büchi Automata via Alternating Automata
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/05_por.pdf
- 30. 3. 2016: Partial Order Reduction - part I
- 6. 4. 2016: Cancelled
- 13. 4. 2016: Partial Order Reduction - part II
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/06_abs.pdf
- 20. 4. 2016: Abstraction - part I
- 27. 4. 2016: Abstraction - part II
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/07_absint.pdf
- 4. 5. 2016: Static Analysis and Abstract Interpretation
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/08_shape.pdf
- 11. 5. 2016: Shape Analysis via 3-Valued Logic [(semi)demo: TVLA output without bug and with bug]
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/1433/jaro2016/IA159/um/09_ultimate.pdf
- 18. 5. 2016: 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/jaro2016/IA159/um/notes.pdf
Následující