FORMAL METHODS · VERIFICATION
形式化验证可视化实验室
通过交互式 SVG 可视化探索形式化方法的核心理论:从模型检测、霍尔逻辑、时序逻辑到定理证明、SAT/SMT 求解、抽象解释、等价性检查与不变式推导。每个模块均可交互,逐步推演验证过程。
01MODEL CHECKING
模型检测
在 Kripke 结构(状态迁移图)上自动验证 CTL 时序性质。枚举可达状态空间,对每条性质求值,不成立时给出反例路径。
Kripke 结构与 CTL 性质验证
02HOARE LOGIC
霍尔逻辑
通过霍尔三元组 {P} S {Q} 描述程序正确性,运用赋值、复合、条件、循环推理规则,从前置条件推导后置条件。
霍尔三元组与推理规则
03TEMPORAL LOGIC
时序逻辑
在线性时序路径上求值 LTL 公式 F(最终)、G(始终)、X(下一刻)、U(直到),观察公式在每个时刻的满足情况。
LTL 公式在路径上的求值
04THEOREM PROVING
定理证明
使用自然演绎推理规则构建证明树,从公理与假设出发,逐步应用推理规则,直至导出目标定理。
自然演绎证明树
05SAT / SMT SOLVING
SAT/SMT 求解
在合取范式(CNF)上运行 DPLL 回溯搜索,构建决策树;遇到冲突时学习冲突子句并回溯,直至判定可满足性。
DPLL 决策树与冲突学习
06ABSTRACT INTERPRETATION
抽象解释
对程序执行区间抽象或符号抽象,将无穷的具体状态域映射到有限的抽象域,安全地近似程序行为。
具体域 vs 抽象域
07EQUIVALENCE CHECKING
等价性检查
将组合电路表示为二元决策图(BDD),通过归约消除冗余节点,判断两个电路在所有输入下是否功能等价。
BDD 归约与电路等价
08INVARIANT INFERENCE
不变式推导
为循环自动推导不变式:从候选不变式出发,通过反例驱动的逐步加强,收敛到足以证明循环正确性的归纳不变式。
循环不变式加强与精化