我一直在阅读有关形式验证的内容，基本观点是它需要一个正式的规范和模型才能使用。然而，许多来源将静态分析归类为一种形式验证技术，一些提到抽象解释并提到它在编译器中的使用。所以我很困惑——如果没有模型的正式描述，这些怎么可能是形式验证？
编辑：我发现的一个来源是：
静态分析：抽象语义是根据预定义的抽象从程序文本中自动计算出来的（有时可以由用户自动/手动定制）
那么这是否意味着它只适用于源代码而无需正式规范？这就是静态分析器所做的。
另外，如果没有形式验证，是否可以进行静态分析？例如，SonarQube 真的执行形式化方法吗？
在硬件和软件系统的上下文中，形式验证是使用形式化数学方法证明或反驳系统底层预期算法关于特定形式规范或属性的正确性的行为。
如果没有对模型的正式描述，这些怎么可能是形式验证呢？
静态分析器将生成一段代码的控制/数据流，然后可以应用形式化方法来验证与系统/单元的预期设计模型的一致性。
请注意，建模/正式规范不是static-analysis的一部分。
无论组合在一起，这两种工具在形式验证中都很有用。
例如，如果系统被建模为有限状态机 (FSM)
然后静态分析的结果将有助于形式验证
控制永远不会沿着上述 FSM 模型中不存在的路径流动。
此外，如果可以根据类型定义、数据流、控制流/调用图（即静态分析器可以验证的代码度量）简单地定义模型，那么静态分析本身就足以正式验证该代码符合这样的模型。
注1。上面的黄色区域是静态分析器，用于强制执行诸如编码指南和命名约定之类的东西，即不能影响程序行为的代码方面。
笔记2。上面的红色区域是形式验证，需要额外的步骤，例如 100% 动态代码覆盖、消除未使用和死代码。这些无法使用静态分析器检测/执行。
静态分析在验证系统/单元是否使用语言规范的子集实现以满足系统/单元设计中规定的目标方面非常有效。
例如，如果设计目标是防止堆栈内存超过特定限制，则可以对递归深度应用限制（或完全禁止递归函数调用）。静态分析用于识别此类违反设计目标的行为。
在没有来自静态分析器的任何警告的情况下，
系统/单元代码将根据其各自模型的此类设计目标进行正式验证。
例如。汽车软件的 MISRA-C 标准定义了用于汽车系统的 C 子集。
MISRA-C:2012 包含
143 条规则——每条规则都可以使用静态程序分析进行检查。
16 条“指令”对解释更开放，或与过程相关。
静态分析只是意味着“阅读源代码并可能抱怨”。（与“动态分析”相反，意思是“运行程序并可能抱怨某些执行行为”）。
有许多不同类型的可能的静态分析投诉。一种可能的抱怨可能是，
Your source code does not provably satisfy a formal specification
如果静态分析器具有“正式”解释的正式规范、源代码的正式解释以及无法找到合适定理的可信定理证明器，则此投诉将基于形式验证。
您可能从静态分析器中得到的所有其他类型的抱怨几乎都是启发式的意见，也就是说，它们是基于对代码的一些非正式解释（或规范，如果它确实存在的话）。
“重型”静态分析器（例如 Coverity 等）具有非常好的程序模型，但它们不会告诉您您的代码符合规范（它们甚至不会查看您是否有规范）。充其量他们只会告诉您您的代码根据语言做了一些未定义的事情（“取消引用空指针”），甚至这种抱怨并不总是正确的。
诸如 MISRA 之类的所谓“样式检查器”也是静态分析器，但它们的抱怨本质上是“您使用了某个委员会认为是错误形式的构造”。这实际上不是一个错误，它是纯粹的意见。
您当然可以将静态分析归类为一种形式验证。
如果没有对模型的正式描述，这些如何成为形式验证？
对于静态分析工具，模型是隐式的（或在某些工具中，是部分隐式的）。例如，“格式良好的 C++ 程序不会泄漏内存，也不会访问尚未初始化的内存”。这些规则可以来自语言规范，或者来自特定项目的编码标准。