IA159 Formal Verification Methods
Programme
- 17. 2. 2022: Introduction
- 24. 2. 2022: Theorem prover ACL2 [no subject of final examination]
- 3. 3. 2022: Reachability in pushdown systems
- 10. 3. 2022: Cancelled
- 17. 3. 2022: Partial order reduction (part I)
- 24. 3. 2022: Partial order reduction (part II)
- 31. 3. 2022: Abstraction (part I) (prerecorded)
- 7. 4. 2022: Cancelled
- 14. 4. 2022: Abstraction (part II) (prerecorded)
- 21. 4. 2022: Static analysis and abstract interpretation
- 28. 4. 2022: Shape analysis via 3-valued logic
- 5. 5. 2022: Verification via automata, symbolic execution, and interpolation
- 12. 5. 2022: Property directed reachability (PDR/IC3)
- LTL Model Checking of Pushdown Systems
- Translation of LTL to Büchi automata
- Symbolic execution, Backward Symbolic execution, k-induction