User Tools

Site Tools


courses:ssv2024:main

Differences

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

Link to this comparison view

courses:ssv2024:main [2024/10/30 10:12]
tsay2 [Announcements]
courses:ssv2024:main [2025/01/06 21:30] (current)
tsay2 [Announcements]
Line 3: Line 3:
  
 ===== Announcements ===== ===== Announcements =====
-  * 10/29: slides for Predicate Transformers available.+  ​* 2025/01/06: {{courses:​ssv2024:​ssv2024grade.pdf|grade report}} available; please send inquiries/​requests,​ if any, to the instructor by 5PM 1/7 (Tue.). 
 +  * 12/18: papers/​files for the {{courses:​ssv2024:​ssv2024final.pdf|final}} are due 5:30PM. 
 +  * 12/11: {{courses:​ssv:​old_exams.zip|old exams}}. 
 +  * 12/11: {{courses:​ssv2024:​hw7.pdf|HW#​7}} for exercise (not counted toward grade). 
 +  * 12/11: slides for Compositional Reasoning available. 
 +  * 12/03: solutions to homework assignments:​ {{courses:​ssv2024:​hw4_s.pdf|HW#​4}} (revised 12/04), {{courses:​ssv2024:​hw5_s.pdf|HW#​5}}. 
 +  * 12/03: {{courses:​ssv2024:​hw6.pdf|HW#​6}} due on 12/11. 
 +  * 11/27: slides for UNITY and Temporal Verification available. 
 +  * 11/27: slides for the Owicki-Gries Method available. 
 +  * 11/20: {{courses:​ssv2024:​termproject.pdf|Term Project}}: proposals due 12/13 and final results due 12/27. 
 +  * 11/20: slides and an example for Using Frama-C available. 
 +  * 11/13: slides for Frama-C and ACSL available (revised 11/20). 
 +  * 11/06: {{courses:​ssv2024:​hw5.pdf|HW#​5}} due on 11/20. 
 +  * 11/06: slides for Hoare Logic (II): Procedures available. 
 +  * 11/06: solutions to homework assignments:​ {{courses:​ssv2024:​hw3_s.zip|HW#​3}}. 
 +  ​* 10/29: slides for Predicate Transformers available ​(revised 10/30).
   * 10/16: {{courses:​ssv2024:​hw4.pdf|HW#​4}} (revised 10/23) due on 10/30.   * 10/16: {{courses:​ssv2024:​hw4.pdf|HW#​4}} (revised 10/23) due on 10/30.
   * 10/14: slides for Soundness and Completeness of Hoare Logic available (revised 10/23).   * 10/14: slides for Soundness and Completeness of Hoare Logic available (revised 10/23).
Line 15: Line 30:
   * 09/02: {{courses:​ssv2024:​hw0.pdf|HW#​0}} due on 09/11.   * 09/02: {{courses:​ssv2024:​hw0.pdf|HW#​0}} due on 09/11.
   * 09/02: slides for Course Introduction,​ Propositional Logic, and First-Order Logic and a note on Natural Deduction available.   * 09/02: slides for Course Introduction,​ Propositional Logic, and First-Order Logic and a note on Natural Deduction available.
-  * 08/26: this wiki site created to complement the NTU COOL site for this course+  * 08/26: this wiki site created to complement the NTU COOL site for this course
 ===== Instructor ===== ===== Instructor =====
 [[http://​im.ntu.edu.tw/​~tsay/​|Yih-Kuen Tsay (蔡益坤)]],​ NTU IM Dept., 3366-1189, Xtsay@ntu.edu.twX (between the enclosing pair of X'​s) ​ [[http://​im.ntu.edu.tw/​~tsay/​|Yih-Kuen Tsay (蔡益坤)]],​ NTU IM Dept., 3366-1189, Xtsay@ntu.edu.twX (between the enclosing pair of X'​s) ​
Line 44: Line 58:
   * Predicate Transformers (1 week: 10/30) [{{courses:​ssv2024:​predicate_transformers.pdf|slides}}]   * Predicate Transformers (1 week: 10/30) [{{courses:​ssv2024:​predicate_transformers.pdf|slides}}]
   * Procedures: Hoare Logic (II) (1 week: 11/6) [{{courses:​ssv2024:​procedures.pdf|slides}}]   * Procedures: Hoare Logic (II) (1 week: 11/6) [{{courses:​ssv2024:​procedures.pdf|slides}}]
-  * Verification Tools: Frama-C + Plugins (2 weeks: 11/13, 11/20) [slides: {{courses:​ssv2024:​frama-c_acsl.pdf|Frama-C and ACSL}}, {{courses:​ssv2024:​Using-Frama-C.pdf|Using Frama-C}}; examples:​{{courses:​ssv2024:​frama-c-examples.zip|Frama-C ​Examples}}]+  * Verification Tools: Frama-C + Plugins (2 weeks: 11/13, 11/20) [slides: {{courses:​ssv2024:​frama-c_acsl.pdf|Frama-C and ACSL}}, {{courses:​ssv2024:​Using-Frama-C.pdf|Using Frama-C}}; examples:​{{courses:​ssv2024:​frama-c-simple-examples.zip|Simple Examples}}, {{courses:​ssv2024:​frama-c-example.zip|Frama-C ​Example}}]
   * Concurrent, Reactive Systems: Owicki-Gries Method (1 week: 11/27) [{{courses:​ssv2024:​concurrency.pdf|slides}}]   * Concurrent, Reactive Systems: Owicki-Gries Method (1 week: 11/27) [{{courses:​ssv2024:​concurrency.pdf|slides}}]
   * Concurrent, Reactive Systems: UNITY and Linear Temporal Logic (1 week: 12/04) [slides: {{courses:​ssv2024:​UNITY.pdf|UNITY}},​{{courses:​ssv2024:​temporal_verification.pdf|Temporal Verification}}]   * Concurrent, Reactive Systems: UNITY and Linear Temporal Logic (1 week: 12/04) [slides: {{courses:​ssv2024:​UNITY.pdf|UNITY}},​{{courses:​ssv2024:​temporal_verification.pdf|Temporal Verification}}]
Line 69: Line 83:
   - //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, Prentice Hall, 1994.   - //​Programming from Specifications,​ 2nd Edition//, C. Morgan, Prentice Hall, 1994.
-  - Frama-C: https://​www.frama-c.com.+  - Frama-C: https://​www.frama-c.com; Why3: https://​www.why3.org;​ Why3-coq: https://​opam.ocaml.org/​packages/​why3-coq/​.
   - //​[[https://​link.springer.com/​book/​10.1007/​978-3-031-55608-1|Guide to Software Verification with Frama-C]]//,​ Editors: Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, 2024.   - //​[[https://​link.springer.com/​book/​10.1007/​978-3-031-55608-1|Guide to Software Verification with Frama-C]]//,​ Editors: Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, 2024.
   - //​[[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.   - //​[[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.
courses/ssv2024/main.1730254328.txt.gz · Last modified: 2024/10/30 10:12 by tsay2