This shows you the differences between two versions of the page.
courses:ssv2009:main [2009/10/21 09:07] tsay |
courses:ssv2009:main [2010/01/15 17:15] (current) tsay |
||
---|---|---|---|
Line 3: | Line 3: | ||
===== Announcements ===== | ===== Announcements ===== | ||
+ | * Jan. 15: slides for Compositional Reasoning available. | ||
+ | * Dec. 23: solutions to {{courses:ssv2009:hw1s.pdf|HW#1}}, {{courses:ssv2009:hw2s.pdf|HW#2}}, and {{courses:ssv2009:hw3s.pdf|HW#3}} available. | ||
+ | * Dec. 16: slides for Temporal Verification available. | ||
+ | * Dec. 14: slides for the Owicki-Gries Method and UNITY available. | ||
+ | * Dec. 14: slides for Z, B, and Alloy available. | ||
+ | * Dec. 03: slides for the Why tool available. | ||
+ | * Oct. 28: slides for Hoare Logic (II): Procedures available. | ||
* Oct. 21: {{courses:ssv2009:hw4.pdf|HW#4}} due on Oct. 28. | * Oct. 21: {{courses:ssv2009:hw4.pdf|HW#4}} due on Oct. 28. | ||
* Oct. 21: slides for Predicate Transformers available. | * Oct. 21: slides for Predicate Transformers available. | ||
Line 52: | Line 59: | ||
* Procedures (+ Object Orientation) (1 week: 10/28) \\ [{{courses:ssv2009:procedures.pdf|slides}}] | * Procedures (+ Object Orientation) (1 week: 10/28) \\ [{{courses:ssv2009:procedures.pdf|slides}}] | ||
* Logical Proofs in Coq (continued) (1 week: 11/04) | * Logical Proofs in Coq (continued) (1 week: 11/04) | ||
- | * Program Verification Tools: Why and Frama-C (1 week: 11/25) | + | * Program Verification Tools: Why and Frama-C (1 week: 11/25) \\ [{{courses:ssv2009:why.pdf|slides}}] |
* Data Refinement + Formal Methods: Z, B, and Alloy (3 weeks: 11/11, 11/18, 12/02) \\ [slides:{{courses:ssv2009:Z.pdf|Z}}, {{courses:ssv2009:B.pdf|B}}, {{courses:ssv2009:Alloy.pdf|Alloy}}] | * Data Refinement + Formal Methods: Z, B, and Alloy (3 weeks: 11/11, 11/18, 12/02) \\ [slides:{{courses:ssv2009:Z.pdf|Z}}, {{courses:ssv2009:B.pdf|B}}, {{courses:ssv2009:Alloy.pdf|Alloy}}] | ||
* Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/09, 12/16) \\ [slides:{{courses:ssv2009:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2009:UNITY.pdf|UNITY}}, {{courses:ssv2009:temporal_verification.pdf|Temporal Verification}}] | * Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/09, 12/16) \\ [slides:{{courses:ssv2009:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2009:UNITY.pdf|UNITY}}, {{courses:ssv2009:temporal_verification.pdf|Temporal Verification}}] | ||
- | * Selected Topics: Modular/Compositional Reasoning (1 week: 12/23) | + | * Selected Topics: Modular/Compositional Reasoning (1 week: 12/23) \\ [{{courses:ssv2009:compositional_reasoning.pdf|slides}}] |
* **Final** (**2009/12/30**) | * **Final** (**2009/12/30**) | ||
* Selected Topics: Separation Logic (1 week: 2010/01/07) | * Selected Topics: Separation Logic (1 week: 2010/01/07) | ||
- | * Selected Topics: Proof-Carrying Code (1 week: 2010/01/14) | + | * Data Refinement + Formal Methods (continued): VDM (1 week: 2010/01/14) |
===== Grading ===== | ===== Grading ===== |