抽象解释的简短实现示例

Question

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

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

有没有人知道任何这样的例子,也许是从大学课程？

Answer 1

AI基于数学理论名称Galois Connection.理论很简单:

1. 摘要程序的行为.
2. 在抽象级别上执行分析.

Galois connection:关联Actual和Abstract程序.

这是迄今为止关于抽象解释的最佳教程:

Answer 2

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

请参阅此处，这是一个简短的介绍。

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