📘 形式化验证工具链
实战手册 · 30章
01
形式化验证概述
什么是形式化验证
为什么需要
与仿真测试区别
应用场景
02
命题逻辑与谓词逻辑
命题逻辑基础
谓词逻辑基础
量词与约束
逻辑等价
自然演绎
03
模型检测基础
基本原理
Kripke结构
时态逻辑LTL/CTL
算法概述
状态爆炸
04
SAT求解器入门
布尔可满足性
DPLL算法
CDCL算法
MiniSAT实战
SAT应用
05
SMT求解器入门
SMT问题定义
SMT-LIB格式
Z3安装配置
Z3 Python API
SMT应用
06
符号执行基础
符号执行原理
路径约束
与具体执行对比
KLEE工具
实战案例
07
抽象解释基础
抽象域理论
格论基础
不动点理论
区间抽象域
程序分析应用
08
霍尔逻辑与程序验证
霍尔三元组
最弱前置条件
最强后置条件
循环不变式
正确性证明
09
Coq证明助手入门
安装与配置
Gallina语言
策略Tactics
简单定理证明
归纳数据类型
10
Isabelle/HOL入门
安装配置
HOL基础语法
定理证明策略
Isar语言
列表性质证明
11
Spin模型检测器
安装配置
Promela语言
LTL属性
验证流程
分布式算法案例
12
NuSMV模型检测器
安装配置
SMV语言
CTL属性
验证流程
硬件设计案例
13
CBMC有界模型检测
安装配置
C程序建模
断言与假设
循环展开
嵌入式验证
14
Frama-C静态分析
安装配置
ACSL契约
E-ACSL验证
WP插件
值分析插件
15
TLA+形式化规范
安装配置
TLA+语法
Temporal Logic
TLC检测器
分布式系统案例
16
Alloy形式化建模
安装配置
Alloy语法
关系逻辑
谓词与事实
安全策略案例
17
Event-B形式化方法
安装配置
Rodin平台
建模基础
精化机制
交通信号灯案例
18
Z语言形式化规范
Z语法基础
Z模式Schema
结构化规范
Z/EVES工具
图书馆系统案例
19
VDM形式化规范
VDM语言基础
VDM-SL与++
Overture工具
验证与测试
自动售货机案例
20
定理证明实战
自然数算术
列表数据结构
二叉树性质
排序正确性
图论性质
21
程序验证实战
数组越界
空指针解引用
除零错误
内存泄漏
竞态条件
22
安全协议形式化验证
Dolev-Yao模型
Needham-Schroeder
TLS握手协议
区块链共识
零知识证明
23
硬件设计形式化验证
组合逻辑等价
时序逻辑验证
流水线一致性
Cache一致性
总线协议
24
嵌入式系统形式化验证
实时系统时序
中断处理验证
OS调度验证
设备驱动验证
AUTOSAR规范
25
人工智能形式化验证
神经网络鲁棒性
决策树公平性
强化学习策略
自动驾驶决策
AI伦理约束
26
形式化验证与DevOps集成
CI/CD流水线
回归验证策略
增量验证技术
验证报告生成
覆盖率分析
27
形式化验证工具链集成
工具互操作性
通用中间表示
结果交换格式
自动化脚本
统一验证平台
28
形式化验证案例研究
Linux内核模块
航天飞控软件
智能合约安全
医疗设备软件
金融交易系统
29
形式化验证前沿趋势
概率模型检测
量子程序验证
ML辅助验证
云原生验证
与LLM结合
30
综合实战项目
需求分析
规范建模
工具选择
验证执行
结果分析
报告与反思