歴代受賞者一覧

受賞者紹介
小林 直樹(こばやし なおき)
昭和43年11月30日生まれ
東京工業大学大学院情報理工学研究科 助教授

プログラム解析・検証のための先進的型システム

並行プログラムの正しさを検証する技術は、交通管制システム、銀行オンラインシステム、インターネット等の社会基盤を支えるソフトウェアに加えて、医療機器、航空機、自動車、携帯電話を制御する組み込みソフトウェアの信頼性を保証するために不可欠なものとなっている。しかし、並行プログラムのデッドロックの検出やネットワーク等のリソースに対するアクセス様式の検査は、並行プログラムの非決定性のために通常のテスト実行によるデバッグが極めて難しい。その結果、網羅的な誤りの発見が行われずに、危険性を残存したままの並行プログラムが使用されているのが現状である。

小林直樹氏は、並行プログラムの正しさを静的に保証する型システムの定式化を行い、並行プログラムのさまざまな性質を、プログラムの実行前に網羅的かつ機械的に検証することを可能にした。特に、並行プログラムを数学的にモデル化した計算体系であるπ計算に対して型システムを定式化することにより、リソースに対するアクセスを静的に解析することを可能にした研究は、リソースへのアクセス様式を型として表現するという点において、従来の型の概念を大きく発展させたものであり、並行プログラムの理論に対する貢献として極めて大きい。さらに、小林直樹氏が定式化した型システムのアイデアが、マイクロソフト研究所をはじめとして、海外で進んでいる実用化プロジェクトにも取り入れられていることは、理論的な本質を貫いた研究成果は実用にも直結するからに他ならない。

以上の一連の研究成果は、ソフトウェア基礎理論分野において優れた論文が発表され最もレベルの高いとされるInformation and Computation(2編)、ACM Transaction on Programming Language and Systems(2編)、Theoretical Computer Science(2編)などに掲載され、世界中の研究者により非常に多く引用されている。さらに、2001年にはIFIP TC2 Awardを授賞するなど、氏の研究成果は世界的に極めて高く評価されるところとなっている。

※所属名および役職は、受賞時のものです。