This shows you the differences between two versions of the page.
courses:ssv2009:main [2009/09/17 00:26] 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: slides for Predicate Transformers available. | ||
+ | * Oct. 19: slides for Soundness and Completeness of Hoare Logic available. | ||
+ | * Oct. 14: {{courses:ssv2009:hw3.pdf|HW#3}} due on Oct. 21. | ||
+ | * Oct. 07: {{courses:ssv2009:hw2.pdf|HW#2}} due on Oct. 14. | ||
+ | * Oct. 07: slides for Hoare Logic available. | ||
+ | * Sep. 30: {{courses:ssv2009:hw1.pdf|HW#1}} due on Oct. 7. | ||
+ | * Sep. 30: slides for Logical Proofs in Coq available. | ||
+ | * Sep. 23: slides for First-Order Logic available for download. | ||
* Sep. 16: {{courses:ssv2009:hw0.pdf|HW#0}} due on Sep. 23. | * Sep. 16: {{courses:ssv2009:hw0.pdf|HW#0}} due on Sep. 23. | ||
- | * Sep. 16: {{courses:ssv2009:ssv2009info.pdf|PDF version}} of this page; slides for Introduction and Propositional Logic and notes on System LK, Example Proofs, and Natural Deduction available for download. | + | * Sep. 16: {{courses:ssv2009:ssv2009info.pdf|PDF version}} of this page (as of today, without subsequent updates); slides for Introduction and Propositional Logic and notes on System LK, Example Proofs, and Natural Deduction available for download. |
Line 41: | Line 57: | ||
* Verification of Sequential Programs: Hoare Logic (2 weeks: 10/07, 10/14) \\ [slides:{{courses:ssv2009:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2009:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2009:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2009:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] | * Verification of Sequential Programs: Hoare Logic (2 weeks: 10/07, 10/14) \\ [slides:{{courses:ssv2009:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2009:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2009:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2009:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] | ||
* Predicate Transformers and Program Derivation (1 week: 10/21) \\ [{{courses:ssv2009:predicate_transformers.pdf|slides}}] | * Predicate Transformers and Program Derivation (1 week: 10/21) \\ [{{courses:ssv2009:predicate_transformers.pdf|slides}}] | ||
- | * Semantic Modeling in Coq (1 week: 10/28) | + | * Procedures (+ Object Orientation) (1 week: 10/28) \\ [{{courses:ssv2009:procedures.pdf|slides}}] |
- | * Program Verification Tools: Why and Frama-C (1 week: 11/04) | + | * Logical Proofs in Coq (continued) (1 week: 11/04) |
- | * Procedures (+ Object Orientation) (1 week: 11/11) \\ [{{courses:ssv2009:procedures.pdf|slides}}] | + | * 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/18, 11/25, 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 ===== |