抽象解释的简短实现示例

Posted 2023-03-31

【中文标题】抽象解释的简短实现示例

【英文标题】：Short implementation examples of abstract interpretation

【发布时间】：2011-02-25 02:10:29

【问题描述】：

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

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

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

【参考方案1】：

AI 基于数学理论名称Galois 连接。原理很简单：

抽象程序的行为。 在抽象级别执行分析。

Galois connection：关联Actual 和Abstract 程序。

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

【参考方案2】：

这里有 Bertot 的这篇论文

Structural abstract interpretation, A formal study using Coq

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

我还看到了一篇 Cousot 论文：

A gentle introduction to formal verification of computer systems by abstract interpretation

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

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

【参考方案3】：

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

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

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

【参考方案4】：

还有MonoREIL，最近开源的工具BinNavi自带。

请参阅here 是一个简短的介绍。

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