K.Ｆunakoshiのホームページ（天文以外の頁） last update:2024年４月2日
-ソフトウェアと数学の接点-
ここでは、ソフトウェア（又はプログラム）の問題に数学的考え方を適用する例として
主に「抽象解釈(Abstract Interpretation)」を取り上げます。抽象解釈については日本語で
分かり易く書かれた資料がないので、この分野の開拓者であるCousotの論文を中心に紹介
します。また、抽象解釈の根底にはスコットのプログラム理論があるのでそれについても紹介
します。
■抽象解釈
１．抽象解釈とは？
２．単純なプログラム例による抽象解釈入門（Cousot初期論文[1977年]を読む）
・目次及び序論
３．Cousot 1976年の論文（プログラムの動的性質の静的決定）紹介
→Cousot初期論文[1977年]の前年の論文。プログラムの抽象解釈の基本的な考え方が
具体例で示されている。
５．抽象解釈の初心者向け解説の紹介
①エコール・ノルマルP.Cousot教授のMITでの抽象解釈紹介資料解説
→2005年にMIT（マサチューセッツ工科大学）で行われた抽象解釈の集中講義(Lecture1～20)
の最初の導入部分(Lecture1)。
②カンサス州立大学D. Schmidt教授の抽象解釈紹介資料解説
→「象の絵」で抽象解釈の概念を説明するなど分かり易い資料。
③抽象解釈とLattice（束）モデル NEW 2024年3月23日
→私がCSP研究会で発表した資料です。
・Patrick Cousort著 Principles of Abstract Interpretaion, 2021, MIT Press.
・Xaver Rival and Kwangkeun Yi著 Introduction to Static Analysis, 2020, MIT Press.
→これまで抽象解釈の纏まった本は殆どありませんでしたが、ようやく本格的な
テキストが２冊出版されました。
・Antoino Mine: Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation,
now Rublishers Inc, 2017
７．フロー・ダイアグラムの束 － Dana Scottの論文紹介
→ソフトウェアのフローダイアグラムの構造を数学の束論により表現できることを示している。
また、無限ループを完備性により説明している。
８．モデル検査における抽象化（工事中）
→Kripke構造間のガロア接続について
９．ガロア接続の由来
１０．（参考）【仏和対訳】ガロアの第一論文（工事中）
■スコットのプログラム理論 NEW
１．中島玲二著 数理情報学入門を読む(1)
ご意見・ご感想は ccr61210(at)syd.odn.ne.jp (atを@にして） まで。