[Back to Teaching]
計算モデル論 (2013年度，蓮尾担当分)
概要
- 夏学期 金曜3限 13:00 - 14:30
- 理学部4号館 1220教室
- 理学部情報科学科 4年生 選択必修 時間割コード: 0510069
- 講義は日本語で行う．
担当教員，講義の内容
- 蓮尾 一郎 講師 (理学部情報科学科)，超準解析を用いたハイブリッド・システムの形式検証
- 萩谷 昌己 教授 (理学部情報科学科)，進化計算・分子計算・生命計算
- 今井 浩 教授 (理学部情報科学科)，量子非局所性と対話証明
以下は蓮尾担当分についての説明．
講義の内容
論文
-
Kohei Suenaga, Ichiro Hasuo: Programming with Infinitesimals: A While-Language for Hybrid System Modeling. ICALP (2) 2011: 392-403
の理解に向けて，次のトピックについて解説．
- ハイブリッド・システムとは？
- 形式的意味論，プログラム論理 (Hoare logic)
- 超準解析入門
- 超準解析を用いたハイブリッド・システム検証
教科書，参考文献
講義の中で指定．
講義の方法
教科書と，各回に配布するハンドアウトに基づき，板書で行う．
- 口頭説明は日本語，板書は英語．
- 各回の内容は，前回の講義時に配布するハンドアウトの中で予告する．予習が推奨される．(ぜひ，少なくとも，電車の中でざっと眺めてきてください)
- 毎回のレポート課題(下参照)は，復習問題が1つ，予習問題が1つ．
スケジュール
- 2013.4.5 (Fri)
プログラム検証入門．次回はスライドの続き，超準解析を用いたアプローチの概説から．
ハンドアウト
スライド： keynote,
pdf,
pdf (4up, for printing).
- 2013.4.19 (Fri)
ハンドアウト
超準解析によるハイブリッド・システム検証，概説．
スライド (ICE 2012 から):
keynote,
pdf,
pdf (4up, for printing).
- 次回は BNF 記法についてさっと解説したあと，超準解析の解析に入ります．
- 超準解析のテキストにはいくつか誤りがあるので，指摘してください．ココ （学内限定） 指摘してくれた人にはボーナスがあります．
- 2013.4.26 (Fri)
ハンドアウト
Davis のまとめ，Section 3 まで．
- 2013.5.1 (Wed)
Los の定理の証明の4行目まで．次回は続きと，downward transfer の使用例，
[Suenaga & Hasuo, 2011] の概要の解説．
ハンドアウト
- 2013.5.10 (Fri)
ハンドアウト （レポート課題も）
- 2013.5.17 (Fri)
五月祭準備のため，午後は講義なし
- 2013.5.24 (Fri)
この回以降萩谷先生ご担当．
- 2013.5.31 (Fri)
- 2013.6.7 (Fri)
- 2013.6.14 (Fri)
- 2013.6.21 (Fri)
- 2013.6.28 (Fri)
- 2013.7.5 (Fri)
- 2013.7.12 (Fri)
- 2013.7.19 (Fri)