abstract-interpretation - 抽象解释的简短实现示例

Question

我正在学习抽象解释的课程，但我还没有看到任何关于理论如何映射到实际代码的示例。

我正在寻找简短的代码示例，我最好不必使用整个编译器。分析不一定有用，我只想看一个分析得到然后实施的例子。

有谁知道任何这样的例子，也许来自大学课程？

Answer 1

AI基于数学理论名称伽罗瓦连接。理论很简单：

1. 抽象程序的行为。
2. 在抽象层次上进行分析。

Galois connection: 把Actual和Abstract程序联系起来。

这是迄今为止我看到的关于抽象解释的最好的教程：

Answer 2

Bertot 有这篇论文

结构抽象解释，使用 Coq 的正式研究

这为使用 Coq Proof Assistant 的简单玩具语言提供了一个抽象解释器的完整实现。我将其用作具体参考，并发现它很有用，尽管有点困难，考虑到主题，这是可以预料的。Coq 是一个很棒的小软件。

我还在 Cousot 论文中看到：

通过抽象解释温和地介绍计算机系统的形式验证

Astrée 中实现的粗略细节（但我相信会有有用的引用来获取完整细节），我对 Astrée 不熟悉，所以实际上并没有阅读该部分，但我认为它符合您的标准。

如果你再遇到，请告诉我！特别想看一个prolog抽象解释器。

Answer 3

也许这个工具对你来说也很有趣： Interproc Analyzer

它是一种非常简单语言的抽象分析器，但提供了过程间分析。您可以尝试分析并获得有关分析程序的数值不变量。源代码可用（OCaml）。

由抽象解释的“创造者”之一帕特里克·库索（Patrick Cousot）（已经在其中一个答案中提到）给出的一个非常彻底和精确的课程： MIT course about Abstract Interpretation。该课程还提供 OCaml 中的作业。

Answer 4

有 MonoREIL，它与最近开源的工具BinNavi 一起提供。

看到这里是一个简短的介绍。

请注意，MonoREIL 框架的上下文不是编译器，而是二进制代码的分析。然而，它已被用于现实世界的应用程序，请参阅本介绍的幻灯片 34 ff（其中包含更正式的背景）。