形式化验证主要分为模型检验(也称为模型检验)和定理证明两种方法。
以下是调查后整理的笔记。
(其中模型检测工具部分，引用了博主yisun03的这篇博客。)
模型检测步骤和工具模型检测步骤：1.抽象系统数学模型转移系统(Trasition system )马尔可夫链(Markov chain ) Kripke结构) Kripke structure )2.该系统
关注系统的任意运行状态及其之间的关系计算树逻辑CTL :
分支时序逻辑用于描述状态的前后关系和分支情况(mu-运算。
关心系统的动作和状态的关系
模型检测工具：1.面向形式化规范语言的模型检测工具SMV符号模型检测工具
SMV用于检测有限状态系统是否满足CTL表达式。
其建模方法是以模块为单元的，模块可以同步或异步组合，模块描述的基本元素包括不确定性选择、状态转移、并行赋值语句。
模型检测的基本方法是用二叉树表示状态转移关系，用计算不动点的方法检测状态的可达性和满足的性质。 33558 www.cs.CMU.edu/~ model check/SMV.html
新的符号模型检测工具
用于SMV重构的模型检测工具
支持计算树逻辑CTL和线性时序逻辑LTL描述的所有规范
基于SAT的有界模型检验技术http://nusmv.fbk.eu/
nuXmv分析同步有限状态和无限状态系统的新符号模型检测工具
扩展到NuSMV
在有限状态下，nuXmv的特征是基于SAT算法的有效验证引擎
在无限状态下，nuXmv的特征是基于SMT的验证技术，与MathSAT5紧密集成的https://nuxmv.fbk.eu/
33558 www.Sina.com/(uppsalauniversityaalborguniversity )时间自动机的模型检测工具
建模仿真验证实时系统的工具http://www.uppaal.org/
斯坦福大学时间验证器(step )
用模型检测器处理子系统验证问题
用定理证明器集中处理结果
不限于有限状态系统
推理方式联合模型检验应用于更广泛的系统中，无限数据域的程序http://www-step.stanford.edu/
一种自动化工具，用于同时操作和分析会计工作台(cwb )系统
可以检验系统模型之间的等价关系、FRE-ORDER关系和系统是否能满足 mu -运算的公式
建模方法使用CCS语言或LOTOS语言的子集
分析给定程序的状态空间，可检测多个语义的等价性和序列性http://home pages.INF.ed.AC.uk/perdita/cwb /
一种形式化验证、集成和仿真验证交互同步(vis )有限状态系统的工具
集成有限状态系统，这些系统的属性http://vlsi.colorado.edu/~vis/
2 .面向源语言的模型检测工具spin (简单模型检测器)显式模型检测工具
SPIN用于检测有限状态系统是否满足PLTL表达式和其他性质，包括可达性和循环。
建模方式是程序单位、程序异步的组合，程序记述的基本要素是赋值语句、条件语句、通信语句、不确定性选择、循环语句。
基本方法是用机器人表示各进程和PLTL表达式，用计算这些机器人组合可接受的语言是否为空的方法检测进程模型是否满足给定的性质。
建模语言为promela(processmetalanguage )，基于流程结构，有类似c语言的结构http://spin root.com/spin/what is pin.html
blast (berkeleylazyabstractionsoftwareverificationtool ) c程序时序安全属性自动验证工具
基于反例引导的抽象求框架检测C语言程序
采用懒惰抽象(lazy abstraction )技术，有效提高了效率http://CSE web.ucsd.edu/~ r jhala/blast.html
「灌篮高手」程式模型侦测工具
将原始C语言程序抽象为布尔过程的验证工作
抽象的程序会保留下来
布尔变量依靠C2bp,Bebop,Newton3个工具分别负责完成抽象、检测和抽象求精任务
https://www.microsoft.com/en-us/research/project/slam/
JPF(Java Path Finder) Java程序验证工具实现了一个MC-JVM来解决内存分配和垃圾回收等问题
http://babelfish.arc.nasa.gov/trac/jpf
VeriSoft 直接测试C源代码
Eraser 能够检测Java代码
Jchecker C程序模型检测工具
基于谓词抽象理论
采用基于谓词抽象的反例引导的抽象求精框架
能够针对C程序源码抽象出模型并完备地搜索其状态空间，以此验证程序的安全属性
最大限度缩减状态空间
Bandera 并发Java程序的模型检测工具
工具平台
基于程序切片技术，将Java程序转换成中间代码
后端接口适应多种模型检测器，包括SPIN和SMV
http://bandera.projects.cs.ksu.edu/
Klocwork InsightPro 可以检测多种语言类型的多种质量缺陷和安全漏洞
CMC 可以检测C语言程序在执行时OS层级的调度
MaceMC 用于检测分布式系统
http://www.macesystems.org/wiki/macemc
Chess 用于检测多线程的Windows程序
https://www.microsoft.com/en-us/research/project/chess-find-and-reproduce-heisenbugs-in-concurrent-programs/
FDRhttps://www.cs.ox.ac.uk/projects/fdr/
Murphi 一种枚举显示状态的模型检测器，针对C语言http://formalverification.cs.utah.edu/Murphi/
MoonWalker 针对.NET应用的模型检测工具
XMC 对JAVA程序中同步操作算法检测
FLAVERS(FLow Analysis for VERification of Systems 针对ADA语言的工具
http://formalverification.cs.utah.edu/Murphi/
Mocha 针对C语言的模型检测工具https://www.cis.upenn.edu/~mocha/
CBMC 针对C语言/C++的模型检测工具http://www.cprover.org/cbmc/
MAGIC(Modular Analysis of proGrams In C) 针对C语言的模型检测工具http://www.cs.cmu.edu/~chaki/magic/
其他模型检测工具 OFMC一种用于安全协议的符号模型检测工具CoPS
持久安全性检测器Rational TauF-SoftIMPACTAstree analysis toolSaturnCalystoTerminatorSATABSTerminatormCRL2(micro Common Representation Language) 并发系统检测工具LTSA(Labeled Transition System Analyzer) 并发系统检测工具Maude 基于逻辑语义的工具ISP MPI程序的检测工具CHIC(Checker for Interface Compatibility) 模块行为兼容性的验证工具MRMC(Markov Reward Model) 对离散和连续时间的马尔可夫激励模型UMLChecker UML模型检测工具BACH(Bounded ReachAblity CHecker) 用于分析线性混成自动机有界可达性分析LDPChecker 针对正环闭合自动机(Positive Loop-closed Automata)检验线性时段性质QRDChecker 针对时段时序逻辑QRDC(Quantified Restrictred Duration Calculs)的检验工具KronosHyTechAUTOABSFeaVer3VMCaSpin 其他分类方式(1) 结合模型检测与定理证明 STeP 符号模型检测 用有序二叉图OBDDs(Ordered Binary Decision Diagrams)描述状态迁移图用布尔逻辑公式描述系统属性 定界模型检测技术(bounded model checking) 依赖于布尔可满足性问题(boolean satisfiability problem, SAT)的求解器在限定步数k内，确定系统是否满足性质。若不能确定，则增加k值，重新进行验证 其他分类方式(2)
基于自动机理论
SPIN基于不动点定理SMV 其他分类方式(3) 针对实时系统的模型检测工具 UPPAAL, Kronos, STeP 针对并发系统的模型检测工具 Spin, JPF, Verisoft 针对混成系统的模型检测工具 HyTech, HySAT, BACH, LDPChecker 定理证明工具 交互式定理证明器（Interactive Theorem Prover） Coq:
https://coq.inria.fr/
Coq是一个形式化证明管理系统。它提供了一种形式化语言来编写数学定义、可执行的算法和定理，并为机器检查证明的半交互式开发提供了一个环境。典型应用包括编程语言属性的认证（例如CompCert编译器认证项目、用于验证C程序的已验证软件工具链或用于并发分离逻辑的Iris框架）、数学的形式化（例如Feit-Thompson定理的完全形式化，或同伦类型理论）和教学。
HOL：https://hol-theorem-prover.org/
HOL 交互式定理证明器是高阶逻辑的证明助手：一个可以证明定理并实现证明工具的编程环境。 内置的决策程序和定理证明器可以自动建立许多简单的定理（用户可能必须自己证明难的定理！） oracle 机制允许访问外部程序，例如 SMT 和 BDD 引擎。 HOL 特别适合作为实现演绎、执行和属性检查组合的平台。