エドマンド・M・クラーク

エドマンド・M・クラーク
生まれる	エドマンド・メルソン・クラーク・ジュニア (1945-07-27)1945年7月27日 米国バージニア州ニューポートニューズ
死亡	2020年12月22日(2020-12-22)（享年75歳） ピッツバーグ、ペンシルベニア州、アメリカ[1]
母校	コーネル大学
知られている	モデルチェック
受賞歴	AMチューリング賞
科学者としてのキャリア
フィールド	コンピュータサイエンス
機関	カーネギーメロン大学
論文	ホーア型公理系に対する完全性定理と不完全性定理 (1976)
博士課程の指導教員	ロバート・リー・コンスタブル
博士課程の学生	E. アレン エマーソン ブヴァネーシュワル・ミシュラ デビッド・L・ディル ケネス・L・マクミラン
Webサイト	詳しくはこちら

エドモンド・メルソン・クラーク・ジュニア（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博士論文賞を受賞した。さらに、彼の研究グループは、初の並列解決定理証明器（Parthenon）と記号計算システムに基づく定理証明器（Analytica）を開発した。^{[5] 2009年には、}全米科学財団 の資金提供を受けて、複雑系の計算モデル化および分析（CMACS）センターの設立を主導した。このセンターには、複数の大学にまたがる研究者チームがおり、抽象解釈とモデル検査を生物学および組み込みシステムに適用しています。

クラークはACMおよびIEEEのフェローでした。1995年にSemiconductor Research Corporationから Technical Excellence Award 、1999 年にカーネギーメロン大学コンピュータサイエンス学部からAllen Newell Award for Excellence in Research を受賞しました。1999年には、記号モデル検査の開発により、Randal Bryant、E. Allen Emerson、Kenneth McMillanとともにACM Paris Kanellakis Awardを共同受賞しました。2004 年には、ハードウェアおよびソフトウェア システムの形式検証に対する重要かつ先駆的な貢献と、これらの貢献がエレクトロニクス業界に与えた多大な影響により、IEEE Computer Society Harry H. Goode Memorial Award を受賞しました。2005年には、ハードウェアおよびソフトウェアの正当性の形式検証への貢献により、全米技術アカデミーに選出されました。2011年にアメリカ芸術科学アカデミーに選出された。2008年には「モデル検査の発明における役割と、この分野で20年以上にわたりリーダーシップを発揮し続けたこと」が認められ、エルブラン賞を受賞した。2012年には、情報科学分野への多大な貢献が認められ、ウィーン工科大学から名誉博士号を授与された。2014年には、フランクリン研究所から「輸送、通信、医療など、幅広いコンピュータシステムの正確性を自動的に検証する技術の構想と開発における主導的な役割」が認められ、バウアー賞と科学業績賞を受賞した。シグマ・サイとファイ・ベータ・カッパの会員であった。

• コンピュータサイエンスの先駆者リスト

ウィキメディア・コモンズには、エドマンド・M・クラークに関連するメディアがあります。

• 数学系譜プロジェクトのエドマンド・M・クラーク
• カーネギーメロン大学のホームページ
• ホームページからのオンライン経歴
• チューリング賞発表
• モデルチェックの本
• CMACSホームページ
• Microsoft Academicによって索引付けされた Edmund M. Clarke の出版物