近年のハードウェアや実装技術の進歩により、計算機科学発の検証手法が実用の問題に応用可能となりつつある。具体的には、SMV、SPINなどのモデル検査系や、Isabelle/HOL, Coqなどの定理証明系などによる形式的検証手法はCPU設計では既に実用として取り込まれており、さらにセキュリティモデルやプログラムなどの形式的検証への利用の実用的可能性が見込まれている。実際、モデル検査では実用的な大規模プログラムのバグ検出、定理証明系でもJavaCardのバイトコードベリファイアやコンパイラの検証などのケーススタディの事例が急増しており、また欧米の大学ではモデル検査系では数年前から、定理証明系については昨年から、カリキュラムに取り入れる大学が急増するなどホットな分野と成りつつある。
【講義の狙い】
講義の狙いは- 形式的検証手法とは何かの理解- 近年広く用いられているモデル検査系SMV、 SPINの導入と利用法の初歩- 近年広く用いられている定理証明系Isabelle/HOL、 MONAと利用法の初歩- セキュリティモデルやプログラム解析・検証への応用事例の紹介である。
可能であれば，持参のPCにインストールしてもらい、講義中に演習を行いたいと考えている。
本講義では、形式的検証法の基礎、ポピュラーな検証ツールを用いた具体的な応用例・ケーススタディを中心として最近の動向を概観する。講義の前半では、モデル検査による比較的簡単な性質の自動検出（解析）の実現法を説明し、さらに大規模なソフトウェアへの応用可能性について紹介する。後半では、定理証明系を主体としてIsabelle/HOL の使い方、およびセキュリティモデルの検証のケーススタディをとりあげる。最後に、定理証明系における研究の広がりについて論じる。
【教科書】 なし
【 参考書】
１．Model Checking (E.M.Clarke, O.Grumberg, D.A.Peled), MIT Press. (ISBN 0262032708)
２．Ch.4 Automata on Infinite Objects, in Handbook on Theoretical Computer Science Vol.B, J. van Leeuwen (eds.), MIT Press 1990.Isabelle/Hol: A Proof Assistant for Higher-Order Logic(T.Nipkow, L.C.Paulson, M.Wenzel, Springer-Verlag LNCS2283, ISBN:3540433767)
３．Introduction to Hol: A Theorem Proving Environment for Higher OrderLogic(M.J.C.Gordon, T.F.Melham, Cambridge Univ Press, I
【講義計画】
1. イントロ
2. Buchi オートマトンにおけるブール演算
3. 時相論理 CTL, CTL*, LTL, TCTL
4. モデル検査系SMVとBDD
5. Bounded Model Checking
6. プログラム解析＝抽象解釈＋モデル検査
7．SOOT/Bandera
8. プッシュダウンモデル検査とその応用
9. 単項二階論理・定理証明系 MONA
10. 時刻認証のセキュリティモデルの検証(MONA)
11. 定理証明系 Isabelle/HOL
12. 定理証明系 Isabelle/HOL（演習）
13. 時刻認証のセキュリティモデルの検証(Isabelle/HOL)
14. 時刻認証のセキュリティモデルの検証(Isabelle/HOL)（演習）
15. 組み合わせ数学における補題の証明とその展望（構成的論理とCurry-Howard 同型）