User Tools
courses:ssv2009:main
Differences
This shows you the differences between two versions of the page.
|
courses:ssv2009:main [2009/09/30 08:36] 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. 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. | ||
| Line 39: | Line 54: | ||
| * Introduction (.5 week: 09/16a) \\ [{{courses:ssv2009:introduction.pdf|slides}}] | * Introduction (.5 week: 09/16a) \\ [{{courses:ssv2009:introduction.pdf|slides}}] | ||
| * Propositional and First-Order Logics (1.5 weeks: 09/16b, 09/23) \\ [slides:{{courses:ssv2009:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2009:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2009:sequent_LK.pdf|System LK}}, {{courses:ssv2009:sequent_proofs.pdf|Example Proofs}}, {{courses:ssv2009:natural_deduction.pdf|Natural Deduction}}] | * Propositional and First-Order Logics (1.5 weeks: 09/16b, 09/23) \\ [slides:{{courses:ssv2009:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2009:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2009:sequent_LK.pdf|System LK}}, {{courses:ssv2009:sequent_proofs.pdf|Example Proofs}}, {{courses:ssv2009:natural_deduction.pdf|Natural Deduction}}] | ||
| - | * Logical Proofs in the Coq Proof Assistant (1 week: 9/30) \\ [{{courses:ssv2009:natural_deduction_in_Coq.pdf|slides}}] [{{courses:ssv2009:natural_deduction_in_Coq.pdf|slides}}] | + | * Logical Proofs in the Coq Proof Assistant (1 week: 9/30) \\ [{{courses:ssv2009:natural_deduction_in_Coq.pdf|slides}}] |
| * 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 ===== | ||
courses/ssv2009/main.1254271015.txt.gz · Last modified: 2009/09/30 08:36 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
