抽象解释的短实现示例

Question

11

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

我正在寻找短小的代码示例，最好不需要处理整个编译器。分析结果不一定有用，我只想看到一个派生和实现分析的示例。

有人知道这样的例子吗？也许来自某个大学课程？

- Jørgen Fogh

4个回答

4

有一篇由Bertot写的论文：

该论文使用Coq证明助手对一个简单玩具语言的抽象解释器进行了全面实现。我用它作为具体参考，并发现它很有用，尽管有点难理解，但这是可以预料的，因为这个主题比较深奥。Coq是一款非常棒的小型软件。

我还在Cousot的一篇论文中发现了：

粗略地介绍了Astrée的实现细节（但我相信会有有用的引文提供完整的细节）。我不熟悉Astrée，所以没有真正阅读那一部分，但我认为它符合您的标准。

如果您遇到其他内容，请告诉我！特别希望看到Prolog抽象解释器。

- Tom

4

也许这个工具对您也很有趣： Interproc 分析器它是一个抽象分析器，用于非常简单的语言，但提供了过程间分析。您可以尝试分析并获取关于已分析程序的数值不变量。源代码可用（OCaml）。

一门真正深入和精确的课程，由抽象解释的“创造者”之一 Patrick Cousot 提供（在回答中已经提到）： MIT 抽象解释课程。该课程还提供 OCaml 的作业。

- Pachelbel

1

有MonoREIL，它是最近开源的BinNavi工具附带的。

在这里查看简短介绍。

请注意，MonoREIL框架的上下文不是编译器，而是二进制代码的分析。然而，它已被用于实际应用程序，请参见此介绍的第34页及其后面的内容（其中包含更多正式的背景）。

- langlauf.io

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- MARYAM · Accepted Answer

AI是基于一种名为Galois连接的数学理论。该理论非常简单：

Galois连接：将实际和抽象程序相关联。

这篇文章是我迄今为止看过的最好的有关抽象解释的教程。