User Tools
courses:ssv2021:main
Differences
This shows you the differences between two versions of the page.
|
courses:ssv2021:main [2021/09/20 16:25] tsay2 [Syllabus/Schedule (with links to slides/notes)] |
courses:ssv2021:main [2022/01/04 23:58] (current) tsay2 [Announcements] |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ===== Announcements ===== | ===== 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. | ||
| + | * 11/03: slides for Soundness and Completeness of Hoare Logic available. | ||
| + | * 10/27: slides for Hoare Logic (I) and two notes available. | ||
| + | * 10/13: slides and a note for Coq available. | ||
| + | * 09/22: slides for Course Introduction, Propositional Logic, and First-Order Logic and a note on Natural Deduction available. | ||
| * 09/20: this website created to complement the NTU COOL site for this course. | * 09/20: this website created to complement the NTU COOL site for this course. | ||
| Line 27: | Line 41: | ||
| ===== Syllabus/Schedule (with links to slides/notes) ===== | ===== Syllabus/Schedule (with links to slides/notes) ===== | ||
| We shall seek to strike a balance between depth and breadth, covering both the foundations and some of the more successful formalisms, techniques, and tools. Below is a tentative list of topics and their schedule: | We shall seek to strike a balance between depth and breadth, covering both the foundations and some of the more successful formalisms, techniques, and tools. Below is a tentative list of topics and their schedule: | ||
| - | * Introduction (.5 week: 09/22a) [{{courses:ssv2021:introduction.pdf|slides}}] | + | * Introduction: Reasoning about Programs (.5 week: 09/22a) [{{courses:ssv2021:introduction.pdf|slides}}] |
| - | * 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}}] | + | * 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}}; {{courses:ssv2021:natural_deduction_tactics.pdf|Tactics for Natural Deduction in Coq}}] | + | * 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}}] |
| - | * Sequential Programs: Hoare Logic (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 and Program Derivation (1 week: 11/10) [{{courses:ssv2021:predicate_transformers.pdf|slides}}] | + | * Predicate Transformers (1 week: 11/10) [{{courses:ssv2021:predicate_transformers.pdf|slides}}] |
| - | * Procedures (+ Object Orientation) (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: 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}}] | * 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}}] | ||
| * Selected Topics: Modular/Compositional Reasoning (1 week: 12/22) [{{courses:ssv2021:compositional_reasoning.pdf|slides}}] | * Selected Topics: Modular/Compositional Reasoning (1 week: 12/22) [{{courses:ssv2021:compositional_reasoning.pdf|slides}}] | ||
| * Selected Topics: Separation Logic (1 week: 12/29) [{{courses:ssv2021:separation_logic.pdf|slides}}] | * Selected Topics: Separation Logic (1 week: 12/29) [{{courses:ssv2021:separation_logic.pdf|slides}}] | ||
| - | * **Final** (**2022/01/05**) | + | * **Final Exam** (**2022/01/05**) |
| * Broader Picture: An Overview of Formal Methods (1 week: 01/12) [{{courses:ssv2021:formal_methods.pdf|slides}}] | * Broader Picture: An Overview of Formal Methods (1 week: 01/12) [{{courses:ssv2021:formal_methods.pdf|slides}}] | ||
| * Wrap-Up Discussions (1 week: 01/19) | * Wrap-Up Discussions (1 week: 01/19) | ||
courses/ssv2021/main.1632126346.txt.gz · Last modified: 2021/09/20 16:25 by tsay2
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 3.0 Unported
