エドムンド・クラーク

エドムンド・メルソン・クラーク・ジュニア

エドムンド・メルソン・クラーク・ジュニア（1945年7月27日 - 2020年12月22日）は、アメリカの計算機科学者として知られ、主にモデル検査の発展に寄与しました。これは、ソフトウェアとハードウェアの設計を形式的に検証する手法であり、彼の研究はこれらの技術を信頼性の高いものにするための基盤を作りました。クラークはカーネギーメロン大学の計算機科学科の教授としても知られています。

経歴

クラークは1967年にバージニア大学から数学の学士号を取得し、1968年にはデューク大学で修士号を取得しました。その後、1976年にはコーネル大学にて計算機科学の博士号を取得。大学での教職を経て、1978年にはハーバード大学に移り、応用科学部で計算機科学の助教授となりました。1982年、彼はカーネギーメロン大学に移籍し、1989年には教授に昇進しました。また、1995年にはCarnegie Mellon School of Computer ScienceでFORE Systemsの教授職を受けました。

悲しいことに、エドムンド・クラークは2020年12月22日に新型コロナウイルス感染症によって亡くなりました。彼の死は、息子のジェームズによってまずTwitterで公表され、その後、カーネギーメロン大学からも公式に発表されました。75歳という年齢での死は多くの人々に衝撃を与えました。

業績

クラークの研究は、主にソフトウェアとハードウェアの検証、及び自動定理証明に焦点を当てていました。彼の博士論文は、特定のプログラミング言語における制御構造がホーア論理的証明システムに適合しないことを示しました。1981年には、指導していたアレン・エマーソンと共に、有限状態並行システムのためのモデル検査技法を初めて提案しました。これによりクラークの研究グループは、ハードウェア検証にモデル検査を適用する先駆者となりました。

また、二分決定図を用いた記号的モデル検査技術の開発も彼の業績の一つです。この技術は、Kenneth McMillanの博士論文のテーマとなり、その成果によりACM博士論文賞を受賞しました。さらに、彼の研究グループは、世界初の並列分析式自動定理証明機Parthenonや、記号的計算システムに基づく自動定理証明機Analyticaを開発しました。

プロとしての評価

クラークは、計算機科学の重要な進展に対する貢献から、ACMとIEEEのフェローに選ばれました。1995年にはSemiconductor Research CorporationからTechnical Excellence Awardを受賞し、1999年にはカーネギーメロン大学からアレン・ニューウェル賞が授与されました。また、同年には、ランダル・ブライアント、アレン・エマーソン、Kenneth McMillanとともにACMパリス・カネラキス実践的理論賞も受賞しました。

さらに、クラークは2004年にIEEE Computer SocietyのHarry H. Goode Memorial Awardを受賞し、その後も全米技術アカデミーの会員となるなど、計算機科学の分野で広く評価されました。彼はまた、Sigma XiおよびPhi Beta Kappaの会員でもあります。クラークの業績は、彼の専門分野における重要な革新となり、多くの後進の研究者たちにも影響を与え続けました。

受賞歴

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

外部リンク

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

もう一度検索