入学志望の学生さんへ
分離論理を用いたソフトウェア検証の理論と実装の研究をしています。
分離論理とはプログラムのメモリーの状態を簡潔に表現できる論理です。
例えばCプログラムで、割り当てられていないメモリを指すポインタにより
値を参照した場合をチェックしたり検証したりすることができます。
(詳しくは [1] にあります。)
この方法は現在もっとも有望なソフトウェア検証の方法のひとつで、
ロンドン大学のグループは大成功を収めています。
(彼らのシステムは [2] から始まっています。)
私たちの目標は、彼らの方法を大きく改良したシステムを達成することです。
研究方法は、数理論理学、プログラム理論の知識をフルに活用して、
よいシステムを理論的に達成し、それを実装することです。
その途上には、様々な(数学的に)面白い問題が出現し、それを解決することになります。
- [1] J.C. Reynolds,
Separation Logic: A Logic for Shared Mutable Data Structures,
In: Proceedings of Seventeenth Annual IEEE Symposium on
Logic in Computer Science (LICS2002) (2002) 55--74.
-
[2] J. Berdine, C. Calcagno, and P. W. O'Hearn,
Symbolic Execution with Separation Logic,
In: Proceedings of APLAS 2005,
Lecture Notes in Computer Science 3780 (2005) 52--68.
ここは、
プログラム理論と
数理論理学
の両方の勉強に打ち込み、同時に
世の中で役に立つ形あるシステムを最終的に達成してみたいという
学生に、最適の場所です。
私をはじめとして世界で活躍する理論研究者に質問したりアドバイスを受けながら、
自分で納得のゆくまでつきつめて勉強することができます。
理論研究を深めたい数学、理論計算機科学関係の学生にも
とてもよい環境です。
また、総合研究大学院大学学生には(社会人学生を除く)全員に
国立情報学研究所から月額数万万円が給付されるので経済的にも楽です。
意欲ある学生は電子メールでコンタクトしてください。
ここでどういう内容が勉強できるかを知るには次のものを眺めてみてください。
これらは現在の研究テーマ「分離論理を用いたソフトウェア検証」には
間接的にしか関係しませんが、このような形の基礎理論が勉強の内容に
なるでしょう。
- [型理論] 龍田 真, 型理論, (近代科学社, 1992.11) 1--82.
私がだいぶ前に書いた型理論の教科書です。本質だけを簡潔に書いてあり
ひとりで読むのは難しいかも知れませんが、このような形の理論がここで
勉強できることが読み取れるでしょう。
- [数理論理] J.R. Schonfield, Mathematical Logic (Addison-Wesley, 1967).
数理論理の本で初学者でも読み始められる本です。
この本のうち証明論に関する部分がここで勉強できます。
- [ラムダ計算] 高橋正子「計算論 計算可能性とラムダ計算」(近代科学社, 1991).
ラムダ計算のよい教科書です。このような形の理論がここで勉強できます。
- [ラムダ計算と型理論] Makoto Tatsuta,
Types for Hereditary Permutators,
NII Technical Report, NII-2007-010E, 2007,
http://research.nii.ac.jp/TechReports/07-010E.html.
私が2007年秋に有名な未解決問題を解いた論文です。
学生がこのようなものを目標として
最終的にはこれに少しでも近づけるよう勉強できる環境があります。
参考となるリンク:
Graduate School Survival Guide