Loading article…
エドモンド・メルソン・クラーク・ジュニア（1945年7月27日 - 2020年12月22日）は、ハードウェアおよびソフトウェア設計を形式的に検証する手法であるモデル検査の開発で知られるアメリカのコンピュータ科学者、学者である。彼はカーネギーメロン大学のFOREシステムズ・コンピュータサイエンス教授を務めた。クラークは、 E・アレン・エマーソン、ジョセフ・シファキスとともに、2007年のACMチューリング賞を受賞した。
バージニア州ニューポートニューズ生まれのクラークは、 1967年にバージニア大学シャーロッツビル校で数学の学士号、 1968年にデューク大学ノースカロライナ州ダーラム校で数学の修士号、 1976年にコーネル大学ニューヨーク州イサカ校でコンピュータサイエンスの博士号を取得した。博士号取得後、デューク大学コンピュータサイエンス学科で2年間教鞭を執った。1978年、マサチューセッツ州ケンブリッジのハーバード大学に移り、応用科学部門でコンピュータサイエンスの助教授を務めた。1982年にハーバード大学を離れ、ペンシルベニア州ピッツバーグのカーネギーメロン大学コンピュータサイエンス学科の教員となった。彼は1989年に正教授に任命された。1995年には、カーネギーメロン大学コンピュータサイエンス学部の寄付講座であるFOREシステム教授職の初代受賞者となった。2008年に大学教授となり、2015年に名誉教授となった。[ 2 ]
クラークは2020年12月、ペンシルベニア州でのCOVID-19パンデミックの最中に75歳でCOVID-19により亡くなった。[ 3 ] [ 4 ]
クラークの研究対象には、ソフトウェアとハードウェアの検証、自動定理証明が含まれていました。博士論文では、特定のプログラミング言語の制御構造には優れたホア型証明システムがないことを証明しました。1981年、クラークと博士課程の学生E.アレン・エマーソンは、有限状態並行システムの検証手法としてモデル検査の使用を初めて提案しました。彼の研究グループは、ハードウェア検証にモデル検査を使用する先駆者となりました。バイナリ決定図を使用した記号モデル検査も彼のグループによって開発されました。この重要な手法は、 ACM博士論文賞を受賞したケネス・L・マクミランの博士論文の主題でした。さらに、彼の研究グループは、最初の並列分解定理証明器（Parthenon）と記号計算システムに基づく定理証明器（Analytica）を開発しました。[ 5 ] 2009年、彼は米国国立科学財団 の資金提供を受けて、複雑システムの計算モデリングと分析（CMACS）センターの設立を主導しました。このセンターには、複数の大学に所属する研究者チームがおり、抽象解釈とモデル検査を生物システムや組み込みシステムに応用している。
クラークはACMとIEEEのフェローでした。 1995年に半導体研究協会から技術優秀賞を、1999年にカーネギーメロン大学コンピュータサイエンス学部から研究優秀賞であるアレン・ニューウェル賞を受賞しました。1999年には、記号モデル検査の開発で、ランダル・ブライアント、エマーソン、マクミランとともにACMパリス・カネラキス賞を共同受賞しました。2004年には、ハードウェアおよびソフトウェアシステムの形式検証への重要かつ先駆的な貢献、そしてこれらの貢献が電子産業に与えた大きな影響に対して、 IEEEコンピュータソサエティのハリー・H・グッド記念賞を受賞しました。2005年には、ハードウェアおよびソフトウェアの正当性の形式検証への貢献により、米国工学アカデミーの会員に選出されました。彼は2011年にアメリカ芸術科学アカデミーの会員に選出された。2008年には「モデル検査の発明における役割と、20年以上にわたる同分野における継続的なリーダーシップ」が認められ、ハーブランド賞を受賞した。2012年には、情報科学分野への卓越した貢献により、ウィーン工科大学から名誉博士号を授与された。2014年には、「輸送、通信、医療など幅広い分野で使用されているコンピュータシステムの正当性を自動的に検証する技術の構想と開発における主導的な役割」が認められ、フランクリン研究所からバウアー賞と科学功績賞を授与された。彼はシグマ・サイとファイ・ベータ・カッパの会員であった。