User Tools

Site Tools


courses:ssv2022:main

Differences

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

Link to this comparison view

courses:ssv2022:main [2022/11/30 13:31]
tsay2 [Announcements]
courses:ssv2022:main [2023/09/04 22:20] (current)
tsay2 [Announcements]
Line 3: Line 3:
  
 ===== Announcements ===== ===== Announcements =====
 +  * 01/08: grade report available; please send inquiries, if any, to the instructor by 2PM 01/09 (Mon.).
 +  * 12/14: {{courses:​ssv:​old_exams.zip|old exams}}.
 +  * 12/13: solutions to homework assignments:​ {{courses:​ssv2022:​hw6_s.zip|HW#​6}}.
 +  * 12/13: slides for Compositional Reasoning available.
 +  * 12/05: slides for UNITY and Temporal Verification available.
 +  * 12/04: solutions to homework assignments:​ {{courses:​ssv2022:​hw4_s.pdf|HW#​4}},​ {{courses:​ssv2022:​hw5_s.pdf|HW#​5}}.
   * 11/30: {{courses:​ssv2022:​hw6.pdf|HW#​6}} due on 12/09.   * 11/30: {{courses:​ssv2022:​hw6.pdf|HW#​6}} due on 12/09.
   * 11/30: slides for the Owicki-Gries Method available.   * 11/30: slides for the Owicki-Gries Method available.
Line 23: Line 29:
  
 ===== Instructor ===== ===== Instructor =====
-[[http://​im.ntu.edu.tw/​~tsay/​|Yih-Kuen Tsay (蔡益坤)]],​ NTU IM Dept., 3366-1189, Xtsay@im.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) ​
  
 ===== Lectures ===== ===== Lectures =====
Line 70: Line 76:
   - //​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.   - //​[[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://​www.frama-c.com/​download/​acsl-tutorial.pdf|ACSL Mini-Tutorial]],​ Virgile Prevosto.
   - //​[[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
courses/ssv2022/main.1669786281.txt.gz · Last modified: 2022/11/30 13:31 by tsay2