エドムンド・クラーク
その興味は主に、ソフトウェアとハードウェアの検証と自動定理証明である。博士論文で、あるプログラミング言語の制御構造がホーア論理的証明システムに適合しないことを示した。1981年、指導していたアレン・エマーソンと共に、有限状態並行システムの検証技法として、モデル検査を使うことを初めて提唱した。クラークの研究グループは、ハードウェア検証にモデル検査を使うことを先駆的に行った。二分決定図を使った記号的モデル検査も、クラークの研究グループが開発したものである。この重要な技法は Kenneth McMillan が博士論文のテーマとし、その論文はACM博士論文賞を受賞した。また、同研究グループは世界初の並列分析式自動定理証明機 (Parthenon) と世界初の記号的計算システムに基づく自動定理証明機 (Analytica) を開発した。
エドムンド・メルソン・クラーク・ジュニア(Edmund Melson Clarke, Jr.、1945年7月27日 - 2020年12月22日)は、アメリカ合衆国の計算機科学者。ハードウェアやソフトウェアの設計を形式的に検証するモデル検査の開発で知られている計算機科学者。カーネギーメロン大学計算機科学科の教授。