This shows you the differences between two versions of the page.
courses:ssv2011:main [2011/10/27 13:30] tsay |
courses:ssv2011:main [2012/01/07 21:37] (current) tsay |
||
---|---|---|---|
Line 3: | Line 3: | ||
===== Announcements ===== | ===== Announcements ===== | ||
+ | * Dec. 26: slides for Why and for Temporal Verification available. | ||
+ | * Dec. 26: {{courses:ssv2011:hw4.pdf|HW#4}} and {{courses:ssv2011:hw5.pdf|HW#5}} due on Dec. 29. | ||
+ | * Dec. 21: slides for Owicki-Gries and for UNITY available. | ||
+ | * Dec. 15: slides for Z and B available. | ||
+ | * Nov. 17: slides for Hoare Logic (II): Procedures available. | ||
+ | * Nov. 03: slides for Predicate Transformers available. | ||
+ | * Nov. 03: {{courses:ssv2011:hw3.pdf|HW#3}} due on Nov. 17. | ||
* Oct. 27: slides for Soundness and Completeness of Hoare Logic available. | * Oct. 27: slides for Soundness and Completeness of Hoare Logic available. | ||
* Oct. 20: {{courses:ssv2011:hw2.pdf|HW#2}} due on Oct. 27. | * Oct. 20: {{courses:ssv2011:hw2.pdf|HW#2}} due on Oct. 27. | ||
Line 42: | Line 49: | ||
* Introduction (.5 week: 09/15a) \\ [{{courses:ssv2011:introduction.pdf|slides}}] | * Introduction (.5 week: 09/15a) \\ [{{courses:ssv2011:introduction.pdf|slides}}] | ||
* Propositional and First-Order Logics (2.5 weeks: 09/15b, 09/22, 09/29) \\ [slides:{{courses:ssv2011:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2011:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2011:natural_deduction.pdf|Natural Deduction}}] | * Propositional and First-Order Logics (2.5 weeks: 09/15b, 09/22, 09/29) \\ [slides:{{courses:ssv2011:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2011:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2011:natural_deduction.pdf|Natural Deduction}}] | ||
- | * Logical Proofs in the Coq Proof Assistant (1 week: 10/06) \\ [{{courses:ssv2011:natural_deduction_in_Coq.pdf|slides}}] | + | * Logical Proofs in the Coq Proof Assistant (1 week: 10/06) \\ [{{courses:ssv2011:natural_deduction_in_Coq.pdf|slides}}; {{courses:ssv2011:natural_deduction_tactics.pdf|Tactics for Natural Deduction in Coq}}] |
* ESWeek + ATVA 2011 (10/09 -- 10/14) | * ESWeek + ATVA 2011 (10/09 -- 10/14) | ||
* Verification of Sequential Programs: Hoare Logic (2 weeks: 10/20, 10/27) \\ [slides:{{courses:ssv2011:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2011:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2011:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2011:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] | * Verification of Sequential Programs: Hoare Logic (2 weeks: 10/20, 10/27) \\ [slides:{{courses:ssv2011:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2011:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2011:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2011:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] |