Differences

This shows you the differences between two versions of the page.

--- courses:ssv2021:main [2021/11/17 05:17] – [Syllabus/Schedule (with links to slides/notes)] tsay2
+++ courses:ssv2021:main [2022/01/04 15:58] (current) – [Announcements] tsay2
@@ Line 3: / Line 3: @@
 ===== Announcements =====
+  * 01/04: {{courses:ssv:old_exams.zip|old exams}}.
+  * 12/29: solutions to homework assignments: {{courses:ssv2021:hw3_s.zip|HW#3}}, {{courses:ssv2021:hw4_s.pdf|HW#4}}, {{courses:ssv2021:hw5_s.pdf|HW#5}}.
+  * 12/22: solutions to homework assignments: {{courses:ssv2021:hw1_s.pdf|HW#1}}, {{courses:ssv2021:hw2_s.pdf|HW#2}}.
+  * 12/22: slides for Compositional Reasoning available.
+  * 12/07: slides for UNITY and the Temporal Verification available.
+  * 12/07: slides for the Owicki-Gries Method available.
+  * 12/01: slides for Frama-C with Coq available.
+  * 11/24: slides for Frama-C and ACSL available.
   * 11/17: slides for Hoare Logic (II): Procedures available.
   * 11/10: slides for Predicate Transformers available.
@@ Line 36: / Line 44: @@
   * Fundamentals: Propositional and First-Order Logics (2.5 weeks: 09/22b, 09/29, 10/06) [slides:{{courses:ssv2021:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2021:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2021:natural_deduction.pdf|Natural Deduction}}]
   * Verification Tools: Coq (2 weeks: 10/13, 10/20) [{{courses:ssv2021:natural_deduction_in_Coq.pdf|slides}}; notes:{{courses:ssv2021:natural_deduction_tactics.pdf|Tactics for Natural Deduction in Coq}}]
-  * Hoare Logic (I): Sequential Programs (2 weeks: 10/27, 11/03) [slides:{{courses:ssv2021:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2021:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2021:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2021:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}]
+  * Sequential Programs: Hoare Logic (I) (2 weeks: 10/27, 11/03) [slides:{{courses:ssv2021:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2021:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2021:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2021:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}]
   * Predicate Transformers (1 week: 11/10) [{{courses:ssv2021:predicate_transformers.pdf|slides}}]
-  * Hoare Logic (II): Procedures (1 week: 11/17) [{{courses:ssv2021:procedures.pdf|slides}}]
+  * Procedures: Hoare Logic (II) (1 week: 11/17) [{{courses:ssv2021:procedures.pdf|slides}}]
-  * Verification Tools: Frama-C + Plugins (2 weeks: 11/24, 12/01) [{{courses:ssv2021:frama-c.pdf|slides}}]
+  * Verification Tools: Frama-C + Plugins (2 weeks: 11/24, 12/01) [slides: {{courses:ssv2021:frama-c_acsl.pdf|Frama-C and ACSL}}, {{courses:ssv2021:frama-c_coq.pdf|Frama-C with Coq}}; examples:{{courses:ssv2021:frama-c_examples.zip|Frama-C Examples}}]
   * Concurrent, Reactive Systems: Owicki-Gries Method (1 week: 12/08) [{{courses:ssv2021:concurrency.pdf|slides}}]
   * Concurrent, Reactive Systems: UNITY and Linear Temporal Logic (1 week: 12/15) [slides: {{courses:ssv2021:UNITY.pdf|UNITY}},{{courses:ssv2021:temporal_verification.pdf|Temporal Verification}}]