我会阅读静态程序分析

静态程序分析是在没有实际执行程序的情况下对计算机软件进行分析（对正在执行的程序进行的分析称为动态分析）。在大多数情况下，分析是针对某个版本的源代码执行的，而在其他情况下是针对某种形式的目标代码执行的。

动态程序分析，

动态程序分析是通过在真实或虚拟处理器上执行程序来执行的计算机软件分析。为了使动态程序分析有效，目标程序必须以足够的测试输入执行以产生有趣的行为

抽象解释，

在计算机科学中，抽象解释是计算机程序语义的合理近似理论，它基于有序集（尤其是格）上的单调函数。它可以被视为计算机程序的部分执行，该程序在不执行所有计算的情况下获得有关其语义（例如控制流、数据流）的信息。

符号执行，

在计算机科学中，符号执行（也称为符号评估）是指通过跟踪符号值而不是实际值来分析程序，这是一种抽象解释。符号模拟领域将相同的概念应用于硬件。符号计算将该概念应用于数学表达式的分析。符号执行用于推理所有在程序中采用相同路径的输入。

符号计算，

在数学和计算机科学中，计算机代数，也称为符号计算或代数计算是一个科学领域，是指研究和开发用于处理数学表达式和其他数学对象的算法和软件。

符号模拟，

在计算机科学中，模拟是对某些适当建模的状态转换系统的执行的计算。通常，此过程在离散线性时间范围内的各个点对系统的完整状态进行建模，从其前身开始按顺序计算每个状态。

模型检查，

在计算机科学中，模型检查又名属性检查是指以下问题：给定一个系统模型，彻底且自动地检查该模型是否满足给定的规范。

可能需要阅读系统保障：超越检测漏洞。

Rolf 可能在这个主题上有很多非常好的投入。在这里阅读他的建议

事实证明，大约一年前，有人在 reddit 上问了大致相同的问题，我发布了一个相当广泛的答案，同时我还在继续编辑它。