エドムンド?メルソン?クラ?ク?ジュニア （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 （著書）