User Tools
courses:sdm2020:main
Differences
This shows you the differences between two versions of the page.
|
courses:sdm2020:main [2020/06/24 11:51] tsay2 [Announcements] |
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) \\ Automata-based model checking, linear temporal logic, Spin (//Promela, never-claims//) \\ [{{courses:sdm2020:automata_based_model_checking.pdf|slides}}]\\ Axiomatic semantics of programs (//assertions, pre/post-conditions, invariants//), partial and total correctness \\ [{{courses:sdm2020:hoare_logic.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 ===== | ||
| Line 105: | Line 106: | ||
| - //Object Constraint Language, OMG Available Specification, Version 2.0//, OMG. | - //Object Constraint Language, OMG Available Specification, Version 2.0//, OMG. | ||
| - //Software Abstractions: Logic, Language, and Analysis//, D. Jackson, MIT Press, 2006. | - //Software Abstractions: Logic, Language, and Analysis//, D. Jackson, MIT Press, 2006. | ||
| + | - //Verification of Sequential and Concurrent Programs, 3rd Edition//, K.R. Apt, F.S. de Boer, and E.-R. Olderog, Springer, 2009. | ||
| + | - [[http://frama-c.com/|Frama-C]]. | ||
| + | - [[http://people.cs.kuleuven.be/~bart.jacobs/verifast/|VeriFast]]. | ||
| - //Temporal Verification of Reactive Systems: Safety//, Z. Manna and A. Pnueli, Springer-Verlag, 1995. | - //Temporal Verification of Reactive Systems: Safety//, Z. Manna and A. Pnueli, Springer-Verlag, 1995. | ||
| - //The SPIN Model Checker: Primer and Reference Manual//, G.J. Holzman, Addison-Wesley, 2003. | - //The SPIN Model Checker: Primer and Reference Manual//, G.J. Holzman, Addison-Wesley, 2003. | ||
| - [[http://spinroot.com/|Spin]]. | - [[http://spinroot.com/|Spin]]. | ||
| - [[http://babelfish.arc.nasa.gov/trac/jpf|Java Pathfinder]]. | - [[http://babelfish.arc.nasa.gov/trac/jpf|Java Pathfinder]]. | ||
| - | - //Verification of Sequential and Concurrent Programs, 3rd Edition//, K.R. Apt, F.S. de Boer, and E.-R. Olderog, Springer, 2009. | ||
| - | - [[http://frama-c.com/|Frama-C]]. | ||
| - | - [[http://people.cs.kuleuven.be/~bart.jacobs/verifast/|VeriFast]]. | ||
| ===== Old Exams and Solutions ===== | ===== Old Exams and Solutions ===== | ||
courses/sdm2020/main.1592970675.txt.gz ยท Last modified: 2020/06/24 11:51 by tsay2
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 3.0 Unported
