- TOP
- 事業のご案内
- 日本学術振興会賞
- 第5回日本学術振興会賞受賞者一覧
- 第5回日本学術振興会賞受賞者
お問い合わせ先
独立行政法人日本学術振興会
総務部 研究者養成課
「日本学術振興会 日本学術振興会賞」担当
〒102-0083
東京都千代田区麹町５－３－１
TEL03(3263)0912
FAX03(3222)1986
過去の受賞者について
第5回（平成20年度）日本学術振興会賞受賞者
 |
|
小林 直樹
|
| （コバヤシ ナオキ） |
| KOBAYASHI Naoki |
| 生年 | 1968年 | 出身地 | 愛知県 | ||||||||||||||||||
| 現職 | 東北大学大学院情報科学研究科 教授 （Professor, Graduate School of Information Sciences, Tohoku University） |
||||||||||||||||||||
| 専門分野 | プログラム理論 | ||||||||||||||||||||
| 略歴 |
|
||||||||||||||||||||
| 授賞理由 | |||||||||||||||||||||
|
「ソフトウェア検証のための型理論」
（Type Theory for Software Verification）
小林直樹氏は、コンピュータで扱うデータの「型」について独創的な理論的展開を行い、これをソフトウェアの検証に応用することで、情報処理の信頼性・安全性・効率を飛躍的に高めるための理論的基盤を構築した。同氏は、数理科学的な検証手法の中でも、特に型（タイプ）の理論に注目し、従来の「整数型」「実数型」「文字列型」などのデータの性質に基づく「型」の考え方を、「データがどのようにアクセスされるのか」にまで拡張することによって、並行して実行される多数のプログラムが本当に正しく動作しているかどうかを検証することを可能にした。また、同じく「型」の拡張によって、暗証番号などの機密情報の安全性に関する検証の理論を発展させ、さらに、プログラム実行の高速化のためのプログラム変換技術についても大きな質的向上をもたらした。 同氏の業績は、理論的に奥深く独創的であるとともに、昨今大きな問題となっている情報インフラストラクチャの安全性・信頼性を飛躍的に高める技術としても高く評価できる。実社会に与える影響も極めて大きく、同研究の更なる発展が期待される。 |
|||||||||||||||||||||
