黄文超

个人信息Personal Information

副教授

博士生导师

硕士生导师

教师拼音名称:huangwenchao

电子邮箱:

形式化方法导引

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

 课件(2024年春,课件在持续更新,请及时下载最新版本)

0.课前准备

PPT

1.绪论

PPTNote

2.经典数理逻辑--问题定义

PPTNote

3.经典数理逻辑--问题求解基础

PPTNote

4.逻辑问题求解

(SAT/SMT)

应用

PPTNote

理论

SAT求解

PPTNote

SMT求解

PPTNote

CNF与Horn Clauses

PPTNote

5.模型检测

应用

Model checking | LTL | CTL

PPTNote

NuSMV

PPTNote

理论

Basics: Fixpoint | BDD

PPTNote

BMC | K-induction

PPTNote

6. 案例分析

ProVerif: A Verifier of Security Protocols

PPTNote

Software Analysis: AI and CEGAR

PPTNote

Coq

Introduction & Basics

PPTNote

Inductive Declarations

PPTNote

 

 实验简明教程

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

下载