CS 2206, Programming Verification, Spring 2024

Instructor: Qinxiang Cao (曹钦翔)

TAs: Xiwei Wu(吴熙炜)
Lectures
Time: Tuesday 10:00-11:40, Friday 10:00-11:40 (odd weeks)
Location: East Middle Hall (东中院) 1-302
QQ Group: 181792367
Email: caoqinxiang@sjtu.edu.cn


Extended Reading

  1. Pierce, Benjamin, et. al. Software Foundation.
  2. Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction.
  3. Harper, Robert. Practical Foundations for Programming Languages.

Course Supplements

  1. SetsClass库（下载）
  2. CompCert项目中的64位整数库（下载）

Final project

  1. To be released

Lecture Schedule

Week Date Lecture Notes Homework Attachments
1 02/20    课程信息简介. pdf / v    link   
   课后阅读：简单Coq证明与定义【拓展内容】. pdf / v      
02/23    Coq归纳类型. pdf / v    link   
   程序语言的语法. pdf / v      
   课后阅读：用递归函数定义数学性质. pdf / v      
2 02/27    指称语义. pdf / v    link   
3 03/05    link   
   课后阅读：Coq标准库中的自然数. pdf / v      
   基于关系的指称语义. pdf / v      
03/08      
4 03/12    link   
   课后阅读：逻辑命题的证明【拓展内容】. pdf / v      
5 03/19    不动点定理. pdf / v      
03/22    现实程序语言的指称语义. pdf / v      
6 03/26    link   
03/29    霍尔逻辑. pdf / v      
7 04/07      
8 04/09    link   
9 04/16    分离逻辑. pdf      
04/19      
   过程调用. pdf / v    link   
   课后阅读：Coq标准库中的列表. pdf / v      
10 04/23      
11 04/28    验证工具. pdf      
04/30      
12 05/07    大作业信息. pdf