2025年度 (最新) 学院等開講科目 情報理工学院 数理・計算科学系 数理・計算科学コース
ソフトウェア検証論
- 開講元
- 数理・計算科学コース
- 担当教員
- 南出 靖彦
- 授業形態
- 講義 (対面型)
- メディア利用科目
- -
- 曜日・時限
(講義室) - 火5-6 (W8E-306(W832)) / 金5-6 (W8E-306(W832))
- クラス
- -
- 科目コード
- MCS.T509
- 単位数
- 200
- 開講時期
- 2025年度
- 開講クォーター
- 1Q
- シラバス更新日
- 2025年3月19日
- 使用言語
- 英語
シラバス
授業の目的（ねらい）、概要
ソフトウェア検証の基礎となる理論について話題を選んで解説する． プログラムの意味を定義する操作的意味論について紹介し， プログラム検証の基礎となるホーア論理とその健全性・完全性について議論する． その後，モデル検査等のソフトウェア検証技術の基礎となる理論について解説する． モデル検査, 無限語上のオートマトン， LTL, CTL等．
到達目標
ソフトウェア検証の基礎となる理論を理解するとともに，様々な計算モデルへの理解を深める．
キーワード
操作的意味論，ホーア論理，モデル検査，無限語上のオートマトン, 時相論理
学生が身につける力
- 専門力
- 教養力
- コミュニケーション力
- 展開力 (探究力又は設定力)
- 展開力 (実践力又は解決力)
授業の進め方
以下の授業計画に基づき授業を進める． 毎回，講義中に１〜2個程度の演習問題を出し，理解度を確認しながら進める．また，7回程度の演習問題を解く課題を出す．
授業計画・課題
| 授業計画 | 課題 | |
|---|---|---|
| 第1回 | プログラミング言語の操作的意味論 | 操作的意味論： big-step と small-step |
| 第2回 | ホーア論理(1) | ホーア論理の推論規則 |
| 第3回 | ホーア論理（２）：健全性と相対完全性 | 相対完全性, 表明言語の表現力 |
| 第4回 | ホーア論理（3): 実用的側面 | total correctness, verification condition |
| 第5回 | ホーア論理(4)： 検証ツールによる演習 | 検証ツール |
| 第6回 | 命題論理とその充足可能性判定 | 命題論理，SAT |
| 第7回 | 述語論理の復習， エルブランの定理 | 述語論理の意味論， 標準形 |
| 第8回 | 自動証明の原理：導出原理 | 単一化， 導出原理 |
| 第9回 | 無限語上のオートマトン(1) | ω正則現言語, Büchiオートマトン |
| 第10回 | 無限語上のオートマトン(2) | 閉包性， Muller オートマトン |
| 第11回 | 線形時間時相論理(LTL) | LTLの意味論とモデル検査 |
| 第12回 | 分岐時間時相論理(CTL) | CTLの意味論とモデル検査 |
| 第13回 | 二分決定図(BDD) | BDD上の演算 |
| 第14回 | ソフトウェアモデル検査 | 抽象化， 反例による詳細化 |
準備学修(事前学修・復習)等についての指示
学修効果を上げるため，教科書や配布資料等の該当箇所を参照し，「毎授業」授業内容に関する予習と復習（課題含む）をそれぞれ概ね100分を目安に行うこと。
教科書
指定しない．
参考書、講義資料等
講義資料を適宜配付する．
次の本を参考書として使用する．
＊Formal Semantics of Programming Languages, Glynn Winskel, MIT Press, 1993.
＊Automata Theory: An Algorithmic Approach, Javier Esparza and Michael Blondin, MIT Press, 2023.
成績評価の方法及び基準
レポート及び課題の得点により評価する．
関連する科目
- MCS.T214 ： オートマトンと数理言語論
- MCS.T334 ： プログラミング言語処理系
- MCS.T313 ： 数理論理学
- MCS.T404 ： 計算論理学
履修の条件・注意事項
論理，オートマトン，文脈自由文法に関する基礎的な知識を仮定する．
ソフトウェア検証に関する演習を各自のPCで行う．演習が可能な環境：Mac OS, Linux, Windows などの上の Docker．