abstract-interpretation - 抽象解釈の短い実装例

Question

私は抽象解釈のコースを受講していますが、理論が実際のコードにどのようにマッピングされるかの例を見たことがありません。

できればコンパイラ全体を操作する必要のない短いコード例を探しています。分析が有用である必要はありません。分析が導出されてから実装される例を見たいだけです。

おそらく大学のコースから、そのような例を知っている人はいますか?

Answer 1

AI数学理論名ガロア接続に基づいています。理論は非常に単純です。

1. プログラムの動作を抽象化します。
2. 抽象的なレベルで分析を実行します。

Galois connectionActual:とAbstractプログラムを関連付けます。

これは、抽象解釈についてこれまでに見た中で最高のチュートリアルです。

Answer 2

Bertotによるこの論文があります

構造抽象解釈、Coqを使った形式研究

これにより、Coq Proof Assistant を使用して単純な玩具言語の抽象インタープリターを完全に実装できます。私はこれを具体的な参考資料として使用しましたが、主題を考えると予想されることですが、少し難しいですが、有用であることがわかりました. Coq は素晴らしい小さなソフトウェアです。

Cousotの論文にも出くわしました：

抽象的な解釈によるコンピュータシステムの正式な検証への穏やかな紹介

Astrée での実装の大まかな詳細 (ただし、完全な詳細については有用な引用があると確信しています)。

また見かけたら教えてください！特にプロローグの抽象インタプリタを見たいです。

Answer 3

このツールも興味深いかもしれません: Interproc Analyzer

非常に単純な言語の抽象アナライザーですが、手続き間の分析を提供します。分析を試して、分析されたプログラムに関する数値的不変条件を取得できます。ソースコードが公開されています (OCaml)。

Abstract Interpretation の「作成者」の 1 人である Patrick Cousot (既に回答の 1 つで言及されています) によって提供された、非常に徹底的で正確なコース: Abstract Interpretation に関する MIT コース。このコースでは、OCaml での課題も提供しています。

Answer 4

最近オープン ソース化されたツールBinNaviに付属している MonoREIL があります。

ここに短いイントロがあります。

MonoREIL フレームワークのコンテキストはコンパイラではなく、バイナリ コードの分析であることに注意してください。それでも、実際のアプリケーションに使用されています。この紹介のスライド 34 以降を参照してください(より正式な背景が含まれています)。