This shows you the differences between two versions of the page.
courses:ssv2014:main [2014/09/18 11:48] tsay [Lectures] |
courses:ssv2014:main [2015/01/08 00:13] (current) tsay [Announcements] |
||
---|---|---|---|
Line 3: | Line 3: | ||
===== Announcements ===== | ===== Announcements ===== | ||
- | * Sep. 18: {{courses:ssv2014:hw0.pdf|HW#0}} due on Sep. 25. | + | * 01/08: solutions to homework assignments: {{courses:ssv2014:hw1s.pdf|HW#1}}, {{courses:ssv2014:hw2s.pdf|HW#2}}, {{courses:ssv2014:hw3s.pdf|HW#3}}. |
- | * Sep. 17: slides for Course Introduction and Propositional Logic and a note on Natural Deduction available. | + | * 01/02: {{courses:ssv:old_exams.zip|old exams}}. |
- | * Sep. 17: this website is the sole source of all up to date course information and syllabus; there will be no separate PDF version. | + | * 12/25: slides for the B-Method available. |
+ | * 12/24: slides for Temporal Verification available. | ||
+ | * 12/24: slides for the Owicki-Gries Method and for UNITY available. | ||
+ | * 12/18: {{courses:ssv2014:hw5.pdf|HW#5}} due on 2015/01/08. | ||
+ | * 12/18: slides for Z available. | ||
+ | * 11/24: {{courses:ssv2014:hw4.pdf|HW#4}} due on 11/27. | ||
+ | * 11/24: {{courses:ssv2014:hw3.pdf|HW#3}}. | ||
+ | * 11/13: slides for Hoare Logic (II): Procedures available. | ||
+ | * 11/01: slides for Soundness and Completeness of Hoare Logic revised. | ||
+ | * 10/30: slides for Predicate Transformers available. | ||
+ | * 10/30: slides for Soundness and Completeness of Hoare Logic available. | ||
+ | * 10/16: slides for Hoare Logic (I) and two notes available. | ||
+ | * 10/10: {{courses:ssv2014:hw2.pdf|HW#2}} due on 10/23. | ||
+ | * 10/10: {{courses:ssv2014:hw1.pdf|HW#1}} due on 10/16. | ||
+ | * 10/09: slides and a note for Logical Proofs in Coq available. | ||
+ | * 09/26: slides for First-Order Logic available. | ||
+ | * 09/18: {{courses:ssv2014:hw0.pdf|HW#0}} due on 09/25. | ||
+ | * 09/17: slides for Course Introduction and Propositional Logic and a note on Natural Deduction available. | ||
+ | * 09/17: this website is the sole source of all up to date course information and syllabus; there will be no separate PDF version. | ||
===== Instructor ===== | ===== Instructor ===== | ||
Line 13: | Line 30: | ||
===== Lectures ===== | ===== Lectures ===== | ||
- | Thursday 3:30-6:20PM, Room 204, College of Management, Building I \\ | + | Thursday 1:20-2:50PM and 5:00-6:00PM, Room 204, College of Management, Building I \\ |
Note: when the class is small enough, we will meet in Room 1108, Management Building II. | Note: when the class is small enough, we will meet in Room 1108, Management Building II. | ||
Line 39: | Line 56: | ||
* Data Refinement + Formal Methods: Z and B (2 weeks: 11/27, 12/04) \\ [slides: {{courses:ssv2014:Z.pdf|Z}}, {{courses:ssv2014:B.pdf|B}}] | * Data Refinement + Formal Methods: Z and B (2 weeks: 11/27, 12/04) \\ [slides: {{courses:ssv2014:Z.pdf|Z}}, {{courses:ssv2014:B.pdf|B}}] | ||
* Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/11, 12/18) \\ [slides:{{courses:ssv2014:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2014:UNITY.pdf|UNITY}}, {{courses:ssv2014:temporal_verification.pdf|Temporal Verification}}] | * Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/11, 12/18) \\ [slides:{{courses:ssv2014:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2014:UNITY.pdf|UNITY}}, {{courses:ssv2014:temporal_verification.pdf|Temporal Verification}}] | ||
- | * **Final** (**2014/12/25**) | + | * Selected Topic: Modular/Compositional Reasoning (1 week: 12/25) \\ [{{courses:ssv2014:compositional_reasoning.pdf|slides}}] |
- | * Selected Topic: Modular/Compositional Reasoning (1 week: 2015/01/08) \\ [{{courses:ssv2014:compositional_reasoning.pdf|slides}}] | + | * **Final** (**2015/01/08**) |
* Selected Topic: Separation Logic (1 week: 2015/01/15) | * Selected Topic: Separation Logic (1 week: 2015/01/15) | ||