黄文超

个人信息Personal Information

副教授

博士生导师

硕士生导师

电子邮箱：

形式化方法导引

当前位置：中文主页 >> 教学课程 >> 形式化方法导引

课件（2024年春，课件在持续更新，请及时下载最新版本）

0.课前准备				PPT
1.绪论				PPT, Note
2.经典数理逻辑--问题定义				PPT, Note
3.经典数理逻辑--问题求解基础				PPT, Note
4.逻辑问题求解 (SAT/SMT)		应用		PPT, Note
		理论	SAT求解	PPT, Note
			SMT求解	PPT, Note
			CNF与Horn Clauses	PPT, Note
5.模型检测	应用	Model checking \| LTL \| CTL		PPT, Note
		NuSMV		PPT, Note
	理论	Basics: Fixpoint \| BDD		PPT, Note
		BMC \| K-induction		PPT, Note
6. 案例分析	ProVerif: A Verifier of Security Protocols			PPT, Note
	Software Analysis: AI and CEGAR			PPT, Note
	Coq	Introduction & Basics		PPT, Note
		Inductive Declarations		PPT, Note

实验简明教程

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	下载