This shows you the differences between two versions of the page.
courses:ssv2020:main [2020/11/11 10:54] tsay2 [Syllabus/Schedule (with links to slides/notes)] |
courses:ssv2020:main [2021/11/09 09:38] (current) tsay2 [Announcements] |
||
---|---|---|---|
Line 3: | Line 3: | ||
===== Announcements ===== | ===== Announcements ===== | ||
+ | * 01/24: grade report available; please send inquiries, if any, to the instructor by 2PM 01/25 (Mon). | ||
+ | * 01/06: solutions to homework assignments final update: {{courses:ssv2020:hw5_s.pdf|HW#5}}. | ||
+ | * 01/05: {{courses:ssv:old_exams.zip|old exams}}. | ||
+ | * 01/03: solutions to HW#4 updated. | ||
+ | * 01/02: solutions to HW#1 updated. | ||
+ | * 12/30: solutions to homework assignments: {{courses:ssv2020:hw1_s.pdf|HW#1}}, {{courses:ssv2020:hw2_s.pdf|HW#2}}, {{courses:ssv2020:hw3_s.zip|HW#3}}, {{courses:ssv2020:hw4_s.pdf|HW#4}}, {{courses:ssv2020:hw6_s.zip|HW#6}} | ||
+ | * 12/23: slides for Compositional Reasoning available. | ||
+ | * 12/23: {{courses:ssv2020:hw7.pdf|HW#7}} for exercise (no credit). | ||
+ | * 12/09: {{courses:ssv2020:hw6.pdf|HW#6}} due on 12/17 at 5PM. | ||
+ | * 12/09: slides for the Temporal Verification available. | ||
+ | * 12/02: slides for the Owicki-Gries Method and for UNITY available. | ||
+ | * 11/25: {{courses:ssv2020:hw5.pdf|HW#5}} due on 12/02. | ||
+ | * 11/25: All examples in the lecture on Why3 available. | ||
+ | * 11/25: [[https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf|Introduction to C program proof with Frama-C and its WP plugin]], by Allan Blanchard. | ||
+ | * 11/25: slides for Frama-C and Why3 available. | ||
+ | * 11/11: slides for Hoare Logic (II): Procedures available. | ||
* 11/11: slides for Soundness and Completeness of Hoare Logic revised. | * 11/11: slides for Soundness and Completeness of Hoare Logic revised. | ||
* 11/04: slides for Predicate Transformers available. | * 11/04: slides for Predicate Transformers available. | ||
Line 41: | Line 57: | ||
* Predicate Transformers and Program Derivation (1 week: 10/28) \\ [{{courses:ssv2020:predicate_transformers.pdf|slides}}] | * Predicate Transformers and Program Derivation (1 week: 10/28) \\ [{{courses:ssv2020:predicate_transformers.pdf|slides}}] | ||
* Procedures (+ Object Orientation) (1 week: 11/04) \\ [{{courses:ssv2020:procedures.pdf|slides}}] | * Procedures (+ Object Orientation) (1 week: 11/04) \\ [{{courses:ssv2020:procedures.pdf|slides}}] | ||
- | * Program Verification Tools: Coq, Why3, and Frama-C (2 weeks: 11/11, 11/18) \\ [slides: {{courses:ssv2020:why.pdf|Why}}, {{courses:ssv2020:frama-c.pdf|Frama-C}}] | + | * Program Verification Tools: Frama-C and Why3 (2 weeks: 11/11, 11/18) \\ [slides: {{courses:ssv2020:frama-c.pdf|Frama-C}}, {{courses:ssv2020:why3.pdf|Why3}}; code: {{courses:ssv2020:why3_examples.zip|Why3 Examples}}] |
* Data Refinement + Formal Methods: Z and B (2 weeks: 11/25, 12/02) \\ [slides: {{courses:ssv2020:Z.pdf|Z}}, {{courses:ssv2020:B.pdf|B}}] | * Data Refinement + Formal Methods: Z and B (2 weeks: 11/25, 12/02) \\ [slides: {{courses:ssv2020:Z.pdf|Z}}, {{courses:ssv2020:B.pdf|B}}] | ||
* Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (3 weeks: 12/09, 12/16, 12/23) \\ [slides:{{courses:ssv2020:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2020:UNITY.pdf|UNITY}}, {{courses:ssv2020:temporal_verification.pdf|Temporal Verification}}] | * Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (3 weeks: 12/09, 12/16, 12/23) \\ [slides:{{courses:ssv2020:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2020:UNITY.pdf|UNITY}}, {{courses:ssv2020:temporal_verification.pdf|Temporal Verification}}] | ||
Line 61: | Line 77: | ||
- //Predicate Calculus and Program Semantics//, E.W. Dijkstra and C.S. Scholten, Springer-Verlag, 1990. | - //Predicate Calculus and Program Semantics//, E.W. Dijkstra and C.S. Scholten, Springer-Verlag, 1990. | ||
- //Programming from Specifications, 2nd Edition//, C. Morgan, 1994. | - //Programming from Specifications, 2nd Edition//, C. Morgan, 1994. | ||
+ | - //[[https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf|Introduction to C program proof with Frama-C and its WP plugin]]//, Allan Blanchard, 2020. | ||
- //[[http://www.cis.upenn.edu/~bcpierce/sf/|Software Foundations]]//, B.C. Pierce, C. Casinghino, M. Greenberg, V. Sjöberg, and B. Yorgey. (Note: click on the link to authors' free download site.) | - //[[http://www.cis.upenn.edu/~bcpierce/sf/|Software Foundations]]//, B.C. Pierce, C. Casinghino, M. Greenberg, V. Sjöberg, and B. Yorgey. (Note: click on the link to authors' free download site.) | ||
- //[[http://adam.chlipala.net/cpdt/|Certified Programming with Dependent Types | - //[[http://adam.chlipala.net/cpdt/|Certified Programming with Dependent Types |