General Information
Fall 2026 · September 15 – December 29, 2026 · 24 sessions.
Class time: 每周二 14:00–15:40；单周五 8:00–9:40。
Location: 闵行校区 东上院202。
See the course calendar for all dates.
LEARNING OBJECTIVES
After learning CDM, the students will understand how to prove correctness and what computers can do and cannot do.
This primary objective is supported by a few others:
- The students will understand the theoretical foundations of formal verification.
- The students will be able to apply tools, such as SMT solvers, to verify program.
- The students will learn if a problem is computable.
Policies
You must work alone on all assignments- You may post questions on Canvas.
- You are encouraged to answer others' questions, but refrain from explicitly giving away solutions.
- Preview assignments due at 14:00 on Tue. & 08:00 on Fri. on the due date
- Review assignments due at 11:59pm on the due date
- Everybody has 5 grace days
- Zero score after the due
Integrity and Collaboration Policy
We will enforce the policy strictly.- The work that you turn in must be yours.
- You must acknowledge your influences.
- You must not look at, or use, solutions from prior years or the Web, or seek assistence from the internet.
- You must take reasonable steps to protect your work. You must not publish your solutions.
- If there are inexplicable discrepancies between exam and lab performance, we will over-weight the exam and interview you.
Staff
Instructor:Zhaoguo Wang: zhaoguowang AT sjtu DOT edu DOT cn
Zeyu Mi: yzmizeyu AT gmail DOT com
TA:
Yuexuan Zhang: zyx2024 AT sjtu DOT edu DOT cn
Wei Huang: boogiepop1230 AT sjtu DOT edu DOT cn
Textbook
- Mathematical Logic and Set Theory, 2nd edition, Chunyi Shi et al., Tsinghua University Press
- 《Introduction to Automata Theory, Languages, and Computation》, John E. Hopcroft, Rajeev Motwani and Jeffrey D. Ullman, Pearson 2001
- Resource of SpongeBob and his best friend (Guess the password ;) or ask your TA)