User Tools
courses:ssv2010:main
Differences
This shows you the differences between two versions of the page.
|
courses:ssv2010:main [2010/09/10 16:09] tsay |
courses:ssv2010:main [2010/12/29 22:06] (current) tsay |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ===== Announcements ===== | ===== Announcements ===== | ||
| + | * Dec. 29: slides for Z, B, and Alloy available. | ||
| + | * Dec. 14: slides for Owicki-Gries Method and UNITY Logic available. | ||
| + | * Dec. 14: slides for Why available. | ||
| + | * Nov. 01: {{courses:ssv2010:hw4.pdf|HW#4}} due on Nov. 11. | ||
| + | * Nov. 01: slides for Soundness and Completeness of Hoare Logic, Predicate Transformers, and Hoare Logic of Procedures available. | ||
| + | * Nov. 01: {{courses:ssv2010:hw3.pdf|HW#3}}. | ||
| + | * Oct. 07: slides for Logical Proofs in Coq and Hoare Logic and notes on Hoare Logic available. | ||
| + | * Oct. 07: {{courses:ssv2010:hw2.pdf|HW#2}} due on Oct. 14. | ||
| + | * Sep. 23: slides for First-Order Logic available. | ||
| + | * Sep. 23: {{courses:ssv2010:hw1.pdf|HW#1}} due on Sep. 30. | ||
| + | * Sep. 20: slides for Propositional Logic revised and a note on Natural Deduction available. | ||
| + | * Sep. 16: slides for Introduction and Propositional Logic available. | ||
| * Sep. 10: class meetings moved to Thursday 2:20-5:20PM. | * Sep. 10: class meetings moved to Thursday 2:20-5:20PM. | ||
| * Sep. 09: this website is the sole source of all up to date course information and syllabus; there will be no separate PDF version (unlike in previous years). | * Sep. 09: this website is the sole source of all up to date course information and syllabus; there will be no separate PDF version (unlike in previous years). | ||
| Line 35: | Line 47: | ||
| The goal of this course is to acquaint the students with fundamentals of formal software verification and to prepare them for conducting research in the area. We shall seek to strike a balance between depth and breadth, covering both the foundations and some of the more successful formalisms, | The goal of this course is to acquaint the students with fundamentals of formal software verification and to prepare them for conducting research in the area. 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: | techniques, and tools. Below is a tentative list of topics and their schedule: | ||
| - | * Introduction (.5 week: 09/15a) \\ [{{courses:ssv2010:introduction.pdf|slides}}] | + | * Introduction (.5 week: 09/16a) \\ [{{courses:ssv2010:introduction.pdf|slides}}] |
| - | * Propositional and First-Order Logics (1.5 weeks: 09/15b, 09/29) \\ [slides:{{courses:ssv2010:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2010:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2010:sequent_LK.pdf|System LK}}, {{courses:ssv2010:sequent_proofs.pdf|Example Proofs}}, {{courses:ssv2010:natural_deduction.pdf|Natural Deduction}}] | + | * Propositional and First-Order Logics (1.5 weeks: 09/16b, 09/23) \\ [slides:{{courses:ssv2010:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2010:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2010:natural_deduction.pdf|Natural Deduction}}] |
| - | * Logical Proofs in the Coq Proof Assistant (1 week: 10/06) \\ [{{courses:ssv2010:natural_deduction_in_Coq.pdf|slides}}] | + | * Logical Proofs in the Coq Proof Assistant (1 week: 09/30) \\ [{{courses:ssv2010:natural_deduction_in_Coq.pdf|slides}}] |
| - | * Verification of Sequential Programs: Hoare Logic (2 weeks: 10/13, 10/20) \\ [slides:{{courses:ssv2010:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2010:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2010:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2010:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] | + | * Verification of Sequential Programs: Hoare Logic (2 weeks: 10/07, 10/14) \\ [slides:{{courses:ssv2010:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2010:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2010:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2010:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] |
| - | * Predicate Transformers and Program Derivation (1 week: 10/27) \\ [{{courses:ssv2010:predicate_transformers.pdf|slides}}] | + | * Predicate Transformers and Program Derivation (1 week: 10/21) \\ [{{courses:ssv2010:predicate_transformers.pdf|slides}}] |
| - | * Procedures + Object Orientation (1 week: 11/03) \\ [{{courses:ssv2010:procedures.pdf|slides}}] | + | * Procedures (+ Object Orientation) (1 week: 10/28) \\ [{{courses:ssv2010:procedures.pdf|slides}}] |
| - | * Program Verification Tools: Coq, Why, and Frama-C (2 weeks: 11/10, 11/17) \\ [{{courses:ssv2010:why.pdf|slides}}] | + | * Program Verification Tools: Coq, Why, and Frama-C (3 weeks: 11/04, 11/11, 11/18) \\ [slides: {{courses:ssv2010:why.pdf|Why}}, {{courses:ssv2010:frama-c.pdf|Frama-C}}] |
| - | * Data Refinement + Formal Methods: Z, B, and Event-B (3 weeks: 11/24, 12/01, 12/08) \\ [slides:{{courses:ssv2010:Z.pdf|Z}}, {{courses:ssv2010:B.pdf|B}}, {{courses:ssv2010:Alloy.pdf|Alloy}}] | + | * Data Refinement + Formal Methods: Z, B, and Alloy (3 weeks: 11/25, 12/02, 12/09) \\ [slides:{{courses:ssv2010:Z.pdf|Z}}, {{courses:ssv2010:B.pdf|B}}, {{courses:ssv2010:Alloy.pdf|Alloy}}] |
| - | * Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/15, 12/22) \\ [slides:{{courses:ssv2010:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2010:UNITY.pdf|UNITY}}, {{courses:ssv2010:temporal_verification.pdf|Temporal Verification}}] | + | * Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/16, 12/23) \\ [slides:{{courses:ssv2010:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2010:UNITY.pdf|UNITY}}, {{courses:ssv2010:temporal_verification.pdf|Temporal Verification}}] |
| - | * **Final** (**2010/12/29**) | + | * **Final** (**2010/12/30**) |
| - | * Selected Topic: Modular/Compositional Reasoning (1 week: 2011/01/05) \\ [{{courses:ssv2010:compositional_reasoning.pdf|slides}}] | + | * Selected Topic: Modular/Compositional Reasoning (1 week: 2011/01/06) \\ [{{courses:ssv2010:compositional_reasoning.pdf|slides}}] |
| - | * Selected Topic: Separation Logic (1 week: 2011/01/12) | + | * Selected Topic: Separation Logic (1 week: 2011/01/13) |
| ===== Grading ===== | ===== Grading ===== | ||
courses/ssv2010/main.1284106170.txt.gz · Last modified: 2010/09/10 16:09 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
