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