个人信息Personal Information
副教授
博士生导师
硕士生导师
教师拼音名称：huangwenchao
电子邮箱：
课件（2024年春，课件在持续更新，请及时下载最新版本）
0.课前准备 |
||||
1.绪论 |
||||
2.经典数理逻辑--问题定义 |
||||
3.经典数理逻辑--问题求解基础 |
||||
4.逻辑问题求解 (SAT/SMT) |
应用 |
|||
理论 |
SAT求解 |
|||
SMT求解 |
||||
CNF与Horn Clauses |
||||
5.模型检测 |
应用 |
Model checking | LTL | CTL |
||
NuSMV |
||||
理论 |
Basics: Fixpoint | BDD |
|||
BMC | K-induction |
||||
6. 案例分析 |
ProVerif: A Verifier of Security Protocols |
|||
Software Analysis: AI and CEGAR |
||||
Coq |
Introduction & Basics |
|||
Inductive Declarations |
||||
实验简明教程
Z3 使用教程 |
|
NuSMV 使用教程 |
参考书目
Logic in Computer Science |
|
形式化方法导论 |
|
Formal Methods: An Appetizer |
|
Handbook of Model Checking |
|
Introduction to the Theory of Computation |
|
致命Bug 软件缺陷的灾难与启示 |
实验参考链接
SAT/SMT by Example |
|
NuSMV |
|
ProVerif |
|
Event B |
|
Coq Proof Assistant |
|
CCF A、B类论文 |
常用链接
VNC Viewer |
|
Adobe Reader |
课件（2024年春）
1 绪论 |
||
2. Automata and Languages |
Regular Languages |
|
Context-free Languages |
||
3. Computability Theory |
The Church-Turing Thesis |
|
Decidability |
||
Reducibility |
||
4. Complexity Theory |
Time Complexity |
|
Space Complexity |
||
参考书目
Introduction to the Theory of Computation |
常用链接
Adobe Reader |