可参考论文第39-41页

“通过抽象解释进行代码混淆和恶意软件检测”

M. Dalla Preda 关于正式混淆；或原始论文中的第 4.4 和 4.5 节

《基于抽象解释的程序转换框架的系统设计》

库索和库索。

该理论是正式的，需要比以下解释更多的技术细节，但其想法是：

程序的“有限迹”语义P由 的所有有限迹的集合定义P。跟踪只不过是 的状态的有限序列P，在运行时获得P，逐步通过 的“命令” P。

（你可能注意到，从一个状态，我们可以得到一组可能的下一个状态，因为这个状态下的命令可能是不确定的：它可以从环境中接收一些值）。

要计算 的有限迹语义P，一种方法（在您的书中提到了哪种方法）是使用F从 FinSeqs 到 FinSeqs 定义的函数：

F : FinSeq -> FinSeq

其中FinSeqs是 的所有“状态的有限序列的子集P”（您可能认为每个子集都是 的“有限迹”语义的可能值P）。

这个函数F映射一个子集X的子集X'，使得每个跟踪x'的X'有一丝丝x的X作为后缀（这就是为什么它被称为在Cousot和Cousot的纸“落后”的原因）。特别是，我们有

x' = sj . x
x = si . x1

并且sj必须能够成为 的下一个状态si。函数的最小固定点F，即一些集合Xp使得

F(Xp) = Xp

称为 的跟踪语义P。