[Back to Teaching]
計算モデル論 (2014年度，蓮尾担当分)
概要
- 夏学期 金曜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つ．
スケジュール
- 2014.4.4 (Fri)
萩谷先生ご担当
- 2014.4.18 (Fri)
萩谷先生ご担当
- 2014.4.25 (Fri)
萩谷先生ご担当
- 2014.5.2 (Fri)
蓮尾担当1回目．
プログラム検証入門．次回はスライドの続き，超準解析を用いたアプローチの概説から．
ハンドアウト
スライド： keynote,
pdf,
pdf (4up, for printing).
- 2014.5.9 (Fri)
蓮尾担当2回目．
超準解析を使ったハイブリッドシステム検証の概要から，Davis のまとめへ．次回は Lemma 2.3 から．
ハンドアウト
- 2014.5.16 (Fri)
五月祭のため午後休講．
- 2014.5.23 (Fri)
蓮尾担当3回目．
超実数の構成，諸性質，移転原理イントロ．次回は一階述語論理の体系を導入して，移転原理を証明．
ハンドアウト
- 2014.5.30 (Fri)
萩谷先生ご担当
- 2014.6.6 (Fri)
萩谷先生ご担当
- 2014.6.13 (Fri)
萩谷先生ご担当
- 2014.6.20 (Fri)
蓮尾担当4回目．
ハンドアウト
- 2014.6.27 (Fri)
今井先生ご担当
- 2014.7.4 (Fri)
今井先生ご担当
- 2014.7.9 (Wed)
今井先生ご担当
- 2014.7.11 (Fri)
今井先生ご担当