K.Funakoshiのホームページ(天文以外の頁) last update:2014.12.30
-ソフトウェアと数学の接点-
ここでは、ソフトウェア(又はプログラム)の問題に数学的考え方を適用する例として
主に「抽象解釈(Abstract Interpretation)」を取り上げます。抽象解釈については日本語で
分かり易く書かれた資料がないので、この分野の開拓者であるCousotの論文を中心に紹介
します。
1.抽象解釈とは?
2.単純なプログラム例による抽象解釈入門(Cousot初期論文[1977年]を読む)
・目次及び序論
3.Cousot 1976年の論文(プログラムの動的性質の静的決定)紹介
→Cousot初期論文[1977年]の前年の論文。プログラムの抽象解釈の基本的な考え方が
具体例で示されている。
5.抽象解釈の初心者向け解説の紹介
@エコール・ノルマルP.Cousot教授のMITでの抽象解釈紹介資料解説
→2005年にMIT(マサチューセッツ工科大学)で行われた抽象解釈の集中講義(Lecture1〜20)
の最初の導入部分(Lecture1)。
Aカンサス州立大学D. Schmidt教授の抽象解釈紹介資料解説
→「象の絵」で抽象解釈の概念を説明するなど分かり易い資料。
6.【仏和対訳】Cousotの2000年の論文(工事中)
7.フロー・ダイアグラムの束 − Dana Scottの論文紹介
→ソフトウェアのフローダイアグラムの構造を数学の束論により表現できることを示している。
また、無限ループを完備性により説明している。
8.モデル検査における抽象化(工事中)
→Kripke構造間のガロア接続について
9.ガロア接続の由来
10.(参考)【仏和対訳】ガロアの第一論文(工事中)
ご意見・ご感想は ccr61210(at)syd.odn.ne.jp (atを@にして) まで。