エドムンド・クラーク

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索
エドムンド・クラーク

エドムンド・メルソン・クラーク・ジュニア(Edmund Melson Clarke, Jr.、1945年7月27日 - )は、ハードウェアやソフトウェアの設計を形式的に検証するモデル検査の開発で知られている計算機科学者。カーネギーメロン大学計算機科学科の教授。アレン・エマーソンジョセフ・シファキスと共に、2007年のACMチューリング賞を受賞。

経歴[編集]

1967年、バージニア大学で数学の学士号を取得。1968年、デューク大学で数学の修士号を取得。1976年、コーネル大学で計算機科学の博士号を取得した。その後2年間、デューク大学計算機科学科で教壇に立った。1978年、ハーバード大学に移り、応用科学部で計算機科学の助教授を務めた。1982年にハーバードを離れ、カーネギーメロン大学の計算機科学科に移った。1989年には教授になっている。1995年、Carnegie Mellon School of Computer ScienceFORE Systems の教授職を最初に受領した。

業績[編集]

その興味は主に、ソフトウェアハードウェアの検証と自動定理証明である。博士論文で、あるプログラミング言語の制御構造がホーア論理的証明システムに適合しないことを示した。1981年、指導していたアレン・エマーソンと共に、有限状態並行システムの検証技法として、モデル検査を使うことを初めて提唱した。クラークの研究グループは、ハードウェア検証モデル検査を使うことを先駆的に行った。二分決定図を使った記号的モデル検査も、クラークの研究グループが開発したものである。この重要な技法は Kenneth McMillan が博士論文のテーマとし、その論文はACM博士論文賞を受賞した。また、同研究グループは世界初の並列分析式自動定理証明機 (Parthenon) と世界初の記号的計算システムに基づく自動定理証明機 (Analytica) を開発した。

プロとしての評価[編集]

クラークはACMIEEEフェローである。1995年には、Semiconductor Research Corporation から Technical Excellence Award を授与され、1999年にはカーネギーメロン大学からアレン・ニューウェル賞を授与された。1999年、ランダル・ブライアントアレン・エマーソン、Kenneth McMillan と共にACMパリス・カネラキス実践的理論賞を受賞した(記号的モデル検査の開発に対して)。2004年、IEEE Computer Society の Harry H. Goode Memorial Award を受賞(ハードウェアおよびソフトウェアシステムの形式的検証への多大な貢献と、それが電子産業にもたらした影響と貢献に対して)。2005年には全米技術アカデミーの会員に選ばれた。また、Sigma XiPhi Beta Kappa の会員でもある。

外部リンク[編集]