エドムンド・クラーク

エドムンド・メルソン・クラーク・ジュニア（Edmund Melson Clarke, Jr.、1945年7月27日 - 2020年12月22日）は、アメリカ合衆国の計算機科学者。ハードウェアやソフトウェアの設計を形式的に検証するモデル検査の開発で知られている計算機科学者。カーネギーメロン大学計算機科学科の教授。

経歴

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

2020年12月22日、新型コロナウイルス感染症（COVID-19）により死去したことが息子のジェームズによるTwitterに、次いでカーネギーメロン大学によって発表された。75歳没^[1]。

業績

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

プロとしての評価

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

受賞歴

• 2007年 - ACMチューリング賞（アレン・エマーソン、ジョセフ・シファキスと共に）
• 2014年 - バウアー賞

脚注

外部リンク

• エドムンド・クラーク - Mathematics Genealogy Project
• カーネギーメロン大学での本人のホームページ
• チューリング賞発表
• Model Checking（著書）