Э. Аллен Эмерсон
Э. Аллен Эмерсон | |
|---|---|
 | |
| Рожденный | 2 июня 1954 г. |
| Гражданство | Соединенные Штаты |
| Образование |
|
| Известный | |
| Награды |
|
| Научная карьера | |
| Поля | Информатика |
| Учреждения | Юта Остин , США |
| Докторантура | Эдмунд М. Кларк |
Эрнест Аллен Эмерсон II (родился 2 июня 1954 года), более известный как Э. Аллен Эмерсон, — американский учёный-компьютерщик , лауреат премии Тьюринга 2007 года . Он является профессором и почетным председателем Регентского совета Техасского университета в Остине , США.
Эмерсон удостоен награды вместе с Эдмундом М. Кларком и Джозефом Сифакисом за изобретение иразработка проверки моделей — метода, используемого при формальной проверке программного и аппаратного обеспечения. [1] Его вклад в темпоральную логику и модальную логику включает введение логики дерева вычислений (CTL). [2] и его расширение CTL* , [3] которые используются при проверке параллельных систем .Он также известен, как и другие, за разработку символьной проверки моделей для решения комбинаторного взрыва , который возникает во многих алгоритмах проверки моделей. [4]
Ранняя жизнь и образование
[ редактировать ]Эмерсон родился в Далласе , штат Техас . Его ранний опыт работы с компьютером включал знакомство с BASIC , Fortran и ALGOL 60 в Дартмутской системе разделения времени и на больших системных компьютерах Burroughs . [1] Затем он получил степень бакалавра наук по математике в Техасском университете в Остине в 1976 году и степень доктора философии по прикладной математике в Гарвардском университете в 1981 году. [1]
Карьера
[ редактировать ]В начале 1980-х годов Эмерсон и его научный руководитель Эдмунд М. Кларк разработали методы проверки системы с конечными состояниями на соответствие формальной спецификации . Они ввели термин «проверка модели» для концепции, которую независимо изучал Джозеф Сифакис в Европе. [1] Этот смысл слова «модель» соответствует использованию теории моделей в математической логике : система называется моделью спецификации.
Работа Эмерсона по проверке моделей включала раннюю и влиятельную темпоральную логику для описания спецификаций и методы уменьшения взрыва пространства состояний. [1]
Награды
[ редактировать ]В 2007 году Эмерсон, Кларк и Сифакис получили премию Тьюринга. [1] Цитата гласит:
за их роль в превращении проверки моделей в высокоэффективную технологию проверки, которая широко применяется в отрасли аппаратного и программного обеспечения.
Помимо премии Тьюринга, Эмерсон получил в 1998 году премию ACM Paris Kanellakis Award .совместно с Рэндалом Брайантом , Кларком и Кеннетом Л. Макмилланом за разработку проверки символических моделей. [4] Цитата гласит:
За изобретение символической проверки моделей — метода формальной проверки системных проектов, который широко используется в индустрии компьютерного оборудования и начинает показывать значительные перспективы также в верификации программного обеспечения и других областях.
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ Jump up to: а б с д и ж «Э. Аллен Эмерсон — лауреат премии А. М. Тьюринга» . amturing.acm.org . Проверено 2 сентября 2022 г.
- ^ Кларк, Эдмунд М.; Эмерсон, Э. Аллен (1982). «Проектирование и синтез скелетов синхронизации с использованием временной логики ветвления» . В Козене, Декстер (ред.). Логика программ . Конспекты лекций по информатике. Том. 131. Берлин, Гейдельберг: Шпрингер. стр. 52–71. дои : 10.1007/BFb0025774 . ISBN 978-3-540-39047-3 .
- ^ Эмерсон, Э. Аллен; Халперн, Джозеф Ю. (2 января 1986 г.). « Возврат к «иногда» и «не никогда»: о ветвлениях и линейной временной логике» . Журнал АКМ . 33 (1): 151–178. дои : 10.1145/4904.4999 . ISSN 0004-5411 . S2CID 10852931 .
- ^ Jump up to: а б «НАГРАДЫ — Э. АЛЛЕН ЭМЕРСОН — «Премия Тьюринга ACM AM» и «Премия Пэрис Канеллакис в области теории и практики » . Ассоциация вычислительной техники . 2015. Архивировано из оригинала 6 июня 2015 года . Проверено 21 июля 2015 г.
[…] автор основополагающих статей, которые положили начало тому, что стало весьма успешной областью проверки моделей.
Внешние ссылки
[ редактировать ]- Домашняя страница Э. Аллена Эмерсона в Техасском университете в Остине
- Э. Аллен Эмерсон в проекте «Математическая генеалогия»
