抽象解釋的簡短實現示例

Question

我正在學習一門關於抽象解釋的課程，但我還沒有看到理論如何映射到實際代碼的任何示例。

我在尋找簡短的代碼示例，我最好不必使用整個編譯器。分析不一定非常有用，我只希望看到一個例子，其中分析得出並實施。

有沒有人知道任何這樣的例子，也許從大學課程？

Answer 1

有MonoREIL，它附帶最近開源工具BinNavi。

查看here是一個簡短的介紹。

請注意，MonoREIL框架的上下文不是編譯器，而是二進制代碼的分析。然而，它已被用於真實世界的應用，請參見幻燈片34 ff this介紹（其中包含更多正式背景）。

Answer 2

有本文由Bertot

Structural abstract interpretation, A formal study using Coq

這給出使用Coq的證明助手簡單的玩具語言的完整實現的抽象解釋的。我用這個作爲具體的參考，並且發現它很有用，雖然有點困難，但是考慮到主題，這是預期的。 Coq是一款非常棒的軟件。

我也是在一個Cousot紙碰到：

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

粗糙的細節（但我相信會有的全部細節有用的引文）在ASTREE實現的，我不熟悉ASTREE ，所以沒有真正閱讀該部分，但我認爲它符合您的標準。

如果你遇到了，請讓我知道！特別希望看到一個序言抽象解釋器。

Answer 3

AI是基於數學理論名稱Galois連接。理論非常簡單：

1. 摘要程序的行爲。
2. 對抽象層次進行分析。

Galois connection：關聯Actual和Abstract程序。

This是迄今爲止關於抽象解釋我所見過的最好的教程：

Answer 4

也許這個工具也是你有意思： Interproc Analyzer

它是一個抽象分析一個非常簡單的語言，然而這提供 過程分析。您可以嘗試分析並獲得有關分析程序的數值不變量。源代碼可用（OCaml）。

一個真正徹底和精確的課程，由抽象解釋的一位「創造者」Patrick Cousot（已經在其中一個答案中提到）提供： MIT course about Abstract Interpretation。課程還提供OCaml中的作業。