Loading article…
E. アレン エマーソン | |
|---|---|
.jpg/500px-E-allen-emerson_(3x4_cropped).jpg) 2022年のエマーソン | |
| 生まれる | 1954年6月2日 |
| 死亡 | 2024年10月15日（満70歳） |
| 教育 | |
| 知られている | |
| 受賞歴 | |
| 科学者としてのキャリア | |
| フィールド | コンピュータサイエンス |
| 機関 | テキサス大学オースティン校 |
| 博士課程の指導教員 | エドマンド・M・クラーク |
アーネスト・アレン・エマーソン2世（1954年6月2日 - 2024年10月15日）は、アメリカのコンピュータ科学者であり、2007年のチューリング賞を受賞しました。彼はテキサス大学オースティン校の教授および理事長を務めていました。
エマーソンは、エドモンド・M・クラーク、ジョセフ・シファキスとともに、ソフトウェアとハードウェアの形式検証に使用される技術であるモデル検査の発明と開発で知られています。 [1]時相論理と様相論理 への彼の貢献には、並行システムの検証に使用される計算木論理（CTL）[2]とその拡張CTL* [ 3]の導入が含まれます。彼はまた、多くのモデル検査アルゴリズムで発生する組み合わせ爆発に対処するために、他の人たちとともにシンボリックモデル検査を開発したことでも知られています。 [4]
幼少期と教育
エマーソンは1954年6月2日、テキサス州ダラスで生まれました。彼は幼い頃からコンピューターに触れ、ダートマスタイムシェアリングシステムやバローズの大規模システムコンピュータでBASIC、Fortran、ALGOL 60に触れていました。[1] その後、1976年にテキサス大学オースティン校で数学の理学士号を取得し、 1981年にハーバード大学で応用数学の博士号を取得しました。 [1]
キャリア
1980年代初頭、エマーソンと彼の博士課程の指導教官であるエドマンド・M・クラークは、有限状態システムを形式仕様に照らして検証する技術を開発しました。彼らはこの概念をモデル検査と名付け、ヨーロッパではジョセフ・シファキスが独自に研究しました。[1]このモデルという言葉の意味は、数理論理学のモデル理論の用法と一致しています。つまり、システムは仕様の モデルと呼ばれます。
エマーソンのモデル検査に関する研究には、仕様を記述するための初期の影響力のある時相論理や、状態空間の爆発を抑える技術が含まれていました。[1]
受賞歴
2007年、エマーソン、クラーク、シファキスはチューリング賞を受賞した。[1]受賞理由は次のとおりです。
モデル検査をハードウェアおよびソフトウェア業界で広く採用されている非常に効果的な検証技術として開発する役割に対して。
チューリング賞に加えて、エマーソンは、記号モデル検査の開発により、ランドール・ブライアント、クラーク、ケネス・L・マクミランとともに1998年のACM パリ・カネラキス賞を受賞した。 [4]表彰状には次のように記されている。
システム設計を形式的に検査する方法であるシンボリックモデル検査の発明に対して。この方法はコンピューターハードウェア業界で広く使用されており、ソフトウェア検証などの分野でも大きな可能性を示し始めています。
死
エマーソンは2024年10月15日にオースティンの自宅で70歳で亡くなった。[5] [6]
参照
参考文献
- ^ abcdef 「E. アレン・エマーソン - AM チューリング賞受賞者」。amturing.acm.org 。 2022年9月2日閲覧。
- ^ Clarke, Edmund M.; Emerson, E. Allen (1982)。「分岐時間時相論理を使用した同期スケルトンの設計と合成」。Kozen, Dexter (編)。プログラムの論理。コンピュータサイエンスの講義ノート。第 131 巻。ベルリン、ハイデルベルク: Springer。pp. 52–71。doi :10.1007/ BFb0025774。ISBN 978-3-540-39047-3。
- ^エマーソン、E .アレン; ハルパーン、ジョセフ Y. (1986 年 1 月 2 日)。「「時々」と「決してない」の再考: 分岐と線形時間時相論理について」。Journal of the ACM。33 ( 1): 151–178。doi : 10.1145 / 4904.4999。ISSN 0004-5411。S2CID 10852931 。
- ^ ab 「AWARDS -- E. ALLEN EMERSON -- 'ACM AM Turing Award' and 'Paris Kanellakis Theory and Practice Award'」。Association for Computing Machinery。2015年。2015年6月6日時点のオリジナルよりアーカイブ。 2015年7月21日閲覧。
[…] モデル検査という非常に成功した分野の基礎を築いた独創的な論文を執筆。
- ^ 「WE BID FAREWELL TO E. ALLEN EMERSON」ハイデルベルク桂冠フォーラム財団。 2024年10月19日閲覧。
- ^ 「アーネスト・アレン・エマーソン2世」ウィード・コーリー・フィッシュ葬儀社・火葬サービス。 2024年10月20日閲覧。
外部リンク
- テキサス大学オースティン校の E. アレン エマーソン ホームページ
- 数学系譜プロジェクトのE.アレン・エマーソン