Грег Нельсон (специалист по информатике)
Грег Нельсон | |
|---|---|
| Рожденный | Чарльз Грегори Нельсон ( 1953-03-27 )27 марта 1953 г. |
| Умер | 2 февраля 2015 г. (2015-02-02)(61 год) |
| Образование | Бакалавр, Гарвардский университет (1976) Доктор философии, Стэнфордский университет (1980) |
| Известный | Выполнимость по модулю теории Расширенная статическая проверка Проверка программ Комитет Modula-3 ESC/Java Simplify доказательство теорем |
| Награды | Премия Эрбрана (2013) |
| Научная карьера | |
| Учреждения | Исследовательский центр Xerox в Пало-Альто (PARC) Корпорация цифрового оборудования (DEC) Центр системных исследований (SRC) Лаборатории Hewlett-Packard |
| Тезис | Методы проверки программ (1980) |
| научный руководитель | Роберт Тарьян |
Чарльз Грегори Нельсон (27 марта 1953 г. – 2 февраля 2015 г.) был американским учёным-компьютерщиком . [1] [2]
Биография
Нельсон вырос в Гонолулу . В детстве он преуспел в гимнастике и теннисе. Он посещал университетскую лабораторную школу. Он получил степень бакалавра по математике в Гарвардском университете в 1976 году. Он получил степень доктора философии по информатике в Стэнфордском университете в 1980 году под руководством Роберта Тарьяна . Он жил в Джуно, Аляска, в течение года, прежде чем окончательно обосноваться в районе залива Сан-Франциско .
Известная работа
Его диссертация «Методы проверки программ » [3] оказала влияние как на проверку программ , так и на автоматическое доказательство теорем , особенно в области, которая сейчас называется теориями выполнимости по модулю , где он внес вклад в методы объединения процедур принятия решений , а также эффективные процедуры принятия решений для ограничений без кванторов в логике первого порядка и алгебре терминов . В 2013 году он получил премию Эрбрана : [4]
за его новаторский вклад в доказательство теорем и проверку программ, в том числе за его основополагающую работу с Дереком Оппеном по объединению процедур выполнимости и алгоритмов быстрого замыкания конгруэнтности, за разработку весьма влиятельного средства доказательства теорем Simplify и за его роль в создании области расширенной статической проверки.
Он сыграл важную роль в разработке Simplify Theorem Prover, используемого ESC/Java . Он внес значительный вклад в ряд других областей. Он внес вклад в область проектирования языков программирования как член комитета Modula-3 . В распределенных системах он внес вклад в Network Objects. Он внес пионерский вклад со своими графическими редакторами на основе ограничений (Juno и Juno-2), оконной системой (Trestle), оптимальной генерацией кода (Denali) и многопоточным программированием (Eraser).
Смотрите также
Ссылки
- ^ Перл, Шарон (февраль 2015 г.). «Грег Нельсон: 27 марта 1953 г. – 2 февраля 2015 г.». Palo Alto Online . Пало-Альто , Калифорния . Получено 15 апреля 2021 г. .
- ^ Перл, Шарон (4 марта 2015 г.). «Грег Нельсон». Honolulu Star-Advertiser: Некрологи . Гонолулу , Гавайи . Получено 15 апреля 2021 г.
- ^ Нельсон, Грег (1980–1981). Методы проверки программ (PDF) . Кафедра электротехники и компьютерных наук (PhD). Калифорнийский университет в Беркли . Получено 13 апреля 2021 г. .
- ^ Монмирай, Валентин; Сатклифф, Джефф (июнь 2013 г.). «Премия Эрбрана: за выдающийся вклад в автоматизированное рассуждение». Конференция по автоматизированной дедукции . Получено 13 апреля 2021 г.
