This shows you the differences between two versions of the page.
courses:sdm2020:main [2020/06/24 11:56] tsay2 [References] |
courses:sdm2020:main [2020/07/26 11:38] (current) tsay2 [Announcements] |
||
---|---|---|---|
Line 3: | Line 3: | ||
===== Announcements ===== | ===== Announcements ===== | ||
+ | * 07/03: grade report available; contact the instructor Yih-Kuen Tsay by 5PM 07/04 if you have any question or request. | ||
* 06/24: slides for Hoare Logic available. | * 06/24: slides for Hoare Logic available. | ||
* 06/03: slides for Logic and OCL available. | * 06/03: slides for Logic and OCL available. | ||
Line 81: | Line 82: | ||
* **Term Project: Final Presentations (2020/06/10)** | * **Term Project: Final Presentations (2020/06/10)** | ||
* **Final Exam (2020/06/17)** | * **Final Exam (2020/06/17)** | ||
- | * **Software Verification: Formal Verification** (2 weeks: 06/24, 07/01)\\ Axiomatic semantics of programs (//assertions, pre/post-conditions, invariants//), partial and total correctness \\ [{{courses:sdm2020:hoare_logic.pdf|slides}}] \\ Automata-based model checking, linear temporal logic, Spin (//Promela, never-claims//) \\ [{{courses:sdm2020:automata_based_model_checking.pdf|slides}}] | + | * **Software Verification: Formal Verification** (2 weeks: 06/24, 07/01)\\ Axiomatic semantics of programs (//assertions, pre/post-conditions, invariants//), partial and total correctness \\ [{{courses:sdm2020:hoare_logic.pdf|slides}}, notes: {{courses:sdm2020:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:sdm2020:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] \\ Automata-based model checking, linear temporal logic, Spin (//Promela, never-claims//) \\ [{{courses:sdm2020:automata_based_model_checking.pdf|slides}}] |
===== Grading ===== | ===== Grading ===== |