2007年、エドマンド・M・クラーク（Edmund M. Clarke）は、ハードウェアおよびソフトウェア設計の形式検証手法であるモデル検査の先駆的な開発により、チューリング賞を受賞しました。彼の研究は、複雑な電子システムの正確性を保証するための厳密な数学的手法を確立し、彼の長い学術的キャリアを通じて、現代のコンピューティングインフラストラクチャの信頼性に対するエンジニアのアプローチを根本的に変えました。
学歴
1945年にニューポートニューズで生まれたクラークは、情報学に転向する前に数学の伝統的な道を歩みました。1967年にバージニア大学で数学の学士号を取得し、1968年にデューク大学で修士号を取得しました。1976年にコーネル大学で計算機科学の博士号を取得して正式な教育を終え、その博士論文ではプログラミング言語の制御構造に対する既存のホーア論理スタイルの証明システムの重大な限界を実証しました。
キャリアの歩み
クラークはカーネギーメロン大学に落ち着く前に、いくつかの主要な機関で職務に就きました。博士号取得後、デューク大学で2年間教鞭をとり、1978年にハーバード大学の助教授に就任しました。1982年、カーネギーメロン大学の計算機科学学部に加わりました。1989年までに正教授となり、1995年には初のFOREシステムズ教授に任命されました。2015年までに名誉教授となりました。
形式検証への貢献
1981年、クラークと彼の学生であるE・アレン・エマーソン（E. Allen Emerson）は、有限状態並行システムを検証するための手法であるモデル検査を導入しました。彼の研究グループはその後、ハードウェア検証手法や二分決定図を用いたシンボリックモデル検査の先駆けとなりました。これらの主要な取り組みに加え、彼のチームは並列解法定理証明器「Parthenon」やシンボリック計算システム「Analytica」を開発しました。2009年には、これらの手法を生物学的および組み込みシステムに応用するための複雑システム計算モデリング・分析センターを設立しました。
専門的評価
クラークの研究は、1998年のパリス・カネラキス賞、2004年のハリー・H・グード記念賞、2008年のハーブランド賞など、数多くの賞を受賞しました。2005年には全米工学アカデミーの会員に、2011年にはアメリカ芸術科学アカデミーの会員に選出されました。2014年には、自動システム検証におけるリーダーシップが評価され、フランクリン研究所からバウワー賞および科学功績賞を授与されました。
基本情報
- 生年月日: 1945年、ニューポートニューズ - 没年月日: 2020年、ピッツバーグ - 学歴: バージニア大学（1967年）、デューク大学（1968年）、コーネル大学（1976年） - 主要分野: 計算機科学 - 主な受賞歴: 2007年 ACMチューリング賞 - 所属: ACM、IEEE、全米工学アカデミー - 学術的拠点: カーネギーメロン大学
読者からの質問
### モデル検査とは何ですか？
ハードウェアおよびソフトウェア設計の正確性を保証するために、クラークとE・アレン・エマーソンによって開発された形式検証手法です。
### クラークは寄付講座の教授でしたか？
はい、1995年からカーネギーメロン大学で初のFOREシステムズ教授を務めました。
