User Tools
courses:ssv2010:main
Differences
This shows you the differences between two versions of the page.
|
courses:ssv2010:main [2010/09/26 09:59] tsay |
courses:ssv2010:main [2010/12/29 22:06] (current) tsay |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ===== Announcements ===== | ===== Announcements ===== | ||
| + | * Dec. 29: slides for Z, B, and Alloy available. | ||
| + | * Dec. 14: slides for Owicki-Gries Method and UNITY Logic available. | ||
| + | * Dec. 14: slides for Why available. | ||
| + | * Nov. 01: {{courses:ssv2010:hw4.pdf|HW#4}} due on Nov. 11. | ||
| + | * Nov. 01: slides for Soundness and Completeness of Hoare Logic, Predicate Transformers, and Hoare Logic of Procedures available. | ||
| + | * Nov. 01: {{courses:ssv2010:hw3.pdf|HW#3}}. | ||
| + | * Oct. 07: slides for Logical Proofs in Coq and Hoare Logic and notes on Hoare Logic available. | ||
| + | * Oct. 07: {{courses:ssv2010:hw2.pdf|HW#2}} due on Oct. 14. | ||
| * Sep. 23: slides for First-Order Logic available. | * Sep. 23: slides for First-Order Logic available. | ||
| * Sep. 23: {{courses:ssv2010:hw1.pdf|HW#1}} due on Sep. 30. | * Sep. 23: {{courses:ssv2010:hw1.pdf|HW#1}} due on Sep. 30. | ||
| Line 44: | Line 52: | ||
| * Verification of Sequential Programs: Hoare Logic (2 weeks: 10/07, 10/14) \\ [slides:{{courses:ssv2010:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2010:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2010:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2010:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] | * Verification of Sequential Programs: Hoare Logic (2 weeks: 10/07, 10/14) \\ [slides:{{courses:ssv2010:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2010:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2010:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2010:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] | ||
| * Predicate Transformers and Program Derivation (1 week: 10/21) \\ [{{courses:ssv2010:predicate_transformers.pdf|slides}}] | * Predicate Transformers and Program Derivation (1 week: 10/21) \\ [{{courses:ssv2010:predicate_transformers.pdf|slides}}] | ||
| - | * Procedures + Object Orientation (1 week: 10/28) \\ [{{courses:ssv2010:procedures.pdf|slides}}] | + | * Procedures (+ Object Orientation) (1 week: 10/28) \\ [{{courses:ssv2010:procedures.pdf|slides}}] |
| - | * Program Verification Tools: Coq, Why, and Frama-C (3 weeks: 11/04, 11/11, 11/18) \\ [{{courses:ssv2010:why.pdf|slides}}] | + | * Program Verification Tools: Coq, Why, and Frama-C (3 weeks: 11/04, 11/11, 11/18) \\ [slides: {{courses:ssv2010:why.pdf|Why}}, {{courses:ssv2010:frama-c.pdf|Frama-C}}] |
| - | * Data Refinement + Formal Methods: Z, B, and Event-B (3 weeks: 11/25, 12/02, 12/09) \\ [slides:{{courses:ssv2010:Z.pdf|Z}}, {{courses:ssv2010:B.pdf|B}}] | + | * Data Refinement + Formal Methods: Z, B, and Alloy (3 weeks: 11/25, 12/02, 12/09) \\ [slides:{{courses:ssv2010:Z.pdf|Z}}, {{courses:ssv2010:B.pdf|B}}, {{courses:ssv2010:Alloy.pdf|Alloy}}] |
| * Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/16, 12/23) \\ [slides:{{courses:ssv2010:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2010:UNITY.pdf|UNITY}}, {{courses:ssv2010:temporal_verification.pdf|Temporal Verification}}] | * Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/16, 12/23) \\ [slides:{{courses:ssv2010:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2010:UNITY.pdf|UNITY}}, {{courses:ssv2010:temporal_verification.pdf|Temporal Verification}}] | ||
| * **Final** (**2010/12/30**) | * **Final** (**2010/12/30**) | ||
courses/ssv2010/main.1285466384.txt.gz · Last modified: 2010/09/26 09:59 by tsay
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 3.0 Unported
