General Information
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 8:00am 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:
Zhuohao Shen: ao7777 AT sjtu DOT edu DOT cn
Haoning Lan: sjtulhn AT sjtu DOT edu DOT cn
Textbook
- 《数理逻辑与集合论》第2版，石纯一等著，清华大学出版社
- 《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)