Рэндал Брайант

Американский учёный-компьютерщик (родился в 1952 году)

Рэндал Э. Брайант (родился 27 октября 1952 года) — американский учёный-компьютерщик и учёный, известный своими исследованиями по формальной проверке цифрового оборудования и программного обеспечения . Брайант является преподавателем в Университете Карнеги-Меллона с 1984 года. Он занимал должность декана Школы компьютерных наук (SCS) в Университете Карнеги-Меллона с 2004 по 2014 год. Доктор Брайант вышел на пенсию и стал почётным профессором Founders University 30 июня 2020 года.

Брайант получил множество наград за свои исследования в области верификации оборудования и программного обеспечения, а также алгоритмов и архитектуры компьютеров . Его статья 1986 года о символической булевой манипуляции с использованием упорядоченных бинарных диаграмм решений (BDD) имеет самое большое количество цитирований среди всех публикаций в базе данных Citeseer по литературе по информатике. ^[1] В 2009 году Брайант был награжден премией Фила Кауфмана от консорциума EDA «за его основополагающие технологические прорывы в области формальной верификации».

Ранняя жизнь и образование

Брайант родился 27 октября 1952 года и является сыном Джона Х. Брайанта и Барбары Эверитт Брайант , а также внуком Уильяма Литтелла Эверитта , бывшего декана факультета электротехники Иллинойсского университета в Урбане-Шампейне ( 1949–68). Его сестра — Лоис Брайант, художница по текстилю. Брайант вырос в Бирмингеме, штат Мичиган . Начиная с 1970 года, он учился в Мичиганском университете , где в 1973 году получил степень бакалавра наук по прикладной математике. Его магистерская диссертация по моделированию архитектуры пакетной связи компьютерных систем, опубликованная в 1977 году, известна как одна из первых публикаций по распределенному моделированию. ^[2] Он получил докторскую степень в Массачусетском технологическом институте в 1981 году. ^[3]

Карьера

• С 1981 по 1984 год Брайант был доцентом кафедры компьютерных наук в Калифорнийском технологическом институте . Его исследовательские области включали модели схем VLSI , логическое моделирование и тестирование схем. Он также преподавал курсы по компьютерной архитектуре, теории цифровых систем и компьютерным алгоритмам.
• В 1984 году Брайант присоединился к факультету Карнеги-Меллона в качестве доцента компьютерных наук. Он продолжил свои исследования по моделированию СБИС, проверке схем СБИС, символьной манипуляции и параллельным вычислениям.
• С 1990 по 1991 год он был приглашенным научным сотрудником в Fujitsu Laboratories , Ltd.
• В 1992 году он стал профессором университета Карнеги-Меллон. Брайант преподавал компьютерную архитектуру с 1992 по 1997 год.
• С 2004 по 2014 год он занимал должность декана Школы компьютерных наук в Университете Карнеги — Меллона. За время его пребывания на этом посту общее количество студентов Школы компьютерных наук увеличилось более чем на 50 процентов. ^[4]
• В 2003 году Брайант был избран членом Национальной инженерной академии за вклад в символическое моделирование и логическую проверку.
• С 2011 по 2013 год он входил в состав жюри премии Infosys Prize в области инженерии и компьютерных наук ^[5].
• В 2014–2015 годах он занимал должность помощника директора по исследованиям и разработкам в области информационных технологий в Управлении по научно-технической политике Белого дома , где занимался робототехникой, машинным обучением, высокопроизводительными вычислениями, полупроводниковыми технологиями и облачными вычислениями, а также предоставлял аналитические и консультационные услуги по большим данным.
• В настоящее время Брайант является профессором Школы компьютерных наук . Его последние области исследований включают формальную проверку оборудования и программного обеспечения, системное тестирование и образование в области компьютерных наук. Он преподает курс 15-213: Введение в компьютерные системы вместе с профессором Дэвидом Р. О'Халлароном. Их книга Computer Systems: A Programmer's Perspective , которая знакомит студентов с оборудованием, операционной системой, компилятором и компьютерными сетями, используется более чем в 300 университетах по всему миру.

Исследования и публикации

• За последние годы Брайант провел много исследований по формальной верификации оборудования и программного обеспечения, а также компьютерных систем. Его самая известная публикация ^[6] в 1986 году была «Графовые алгоритмы для манипулирования булевыми функциями» , в которой двоичная диаграмма решений (BDD) была представлена ​​как новая структура данных для представления булевых функций и алгоритмов манипулирования. BDD широко использовались в таких областях, как тестирование и синтез цифровых схем, а также планирование искусственного интеллекта. По словам известного ученого-компьютерщика Дональда Кнута , BDD считались «одной из немногих действительно фундаментальных структур данных, появившихся за последние двадцать пять лет». ^[2] После своих исследований он опубликовал еще одну статью ^[7] по учебнику и обновлению BDD в 1992 году. Его статья о BDD была награждена за самое высокое количество цитирований в базе данных Citeseer среди всех литературных источников по компьютерным наукам. ^[1]
• Его работа по проверке цифровых схем — основополагающая работа — получила многочисленные награды от IEEE и других профессиональных обществ (см. ниже). Его статья « Формальная проверка с помощью символической оценки частично упорядоченных траекторий ^{» [8]} была опубликована в 1995 году. Метод символической оценки траектории, описанный в его статье, был широко принят в отрасли, в частности, используется Intel . ^[3] Начиная с 2004 года Брайант продвигает новые исследовательские инициативы в области вычислений с интенсивным использованием данных.
• Брайант и профессор Дэвид Р. О'Халларон из Университета Карнеги-Меллона вместе написали книгу "Компьютерные системы: точка зрения программиста", в которой они используют новый подход к обучению компьютерным системам. Вместо того, чтобы делать акцент на проектировании и реализации систем, книга фокусируется на обучении студентов тому, как системы - архитектура, компиляторы, операционные системы и компьютерные сети - влияют на поведение и производительность программы. Эта книга, которая сейчас находится в третьем издании, была переведена на корейский, китайский, македонский и русский языки и используется учреждениями по всему миру. ^[9]

Награды и почести

• Брайант является членом IEEE и ACM .
• Он является членом Национальной инженерной академии и Американской академии искусств и наук .
• В 1998 году он получил премию ACM Kanellakis Theory and Practice Award (вместе с Эдмундом М. Кларком , Кеном Макмилланом и Алленом Эмерсоном ).
• В 1989 году ему была присуждена премия IEEE WRG Baker Prize за лучшую статью, опубликованную в любом издании IEEE в предыдущем году (1987).
• В 2007 году Брайант получил премию IEEE Эммануэля Р. Пиоре за исследования инструментов для проверки конструкций полупроводников перед их производством. ^[10]
• В 2009 году Брайант был удостоен премии EDAC/IEEE Phil Kaufman за «основополагающие технологические прорывы в области формальной верификации».
• В 2010 году он получил техническую премию имени А. Ричарда Ньютона в области автоматизации проектирования электроники. ^[11]

Ссылки

1. "Наиболее цитируемые исходные документы". Citeseer . Сентябрь 2006. Получено 5 марта 2007 .
2. "Дом Брайанта". www.cs.cmu.edu . Получено 01.02.2018 .
3. "Рэндал Брайант - Образование и публикации".
4. Университет Карнеги-Меллона. "Пресс-релиз: Бывший декан факультета компьютерных наук Карнеги-Меллона теперь помогает в политическом офисе Белого дома - Новости - Университет Карнеги-Меллона" . Получено 01.02.2018 .
5. "Infosys Prize - Jury 2013". Infosys Science Foundation . Получено 1 марта 2021 г.
6. Брайант, RE (август 1986). «Графовые алгоритмы для манипулирования булевыми функциями». IEEE Transactions on Computers . C-35 (8): 677–691. arXiv : cs/0508044 . doi :10.1109/TC.1986.1676819. ISSN  0018-9340. S2CID  10385726.
7. Брайант, Рэндал Э. (1992-09-01). «Символическая булева манипуляция с упорядоченными диаграммами двоичных решений» (PDF) . ACM Computing Surveys . 24 (3): 293–318. doi :10.1145/136035.136043. ISSN  0360-0300. S2CID  1933530.
8. Сегер, Карл-Йохан Х.; Брайант, Рэндал Э. (1995-03-01). «Формальная верификация с помощью символической оценки частично упорядоченных траекторий». Формальные методы в проектировании систем . 6 (2): 147–189. doi :10.1007/BF01383966. ISSN  0925-9856. S2CID  14804600.
9. Университет Карнеги-Меллона. "Рэндал Брайант - Институт исследований программного обеспечения - Университет Карнеги-Меллона". www.isri.cmu.edu . Получено 01.02.2018 .
10. "IEEE Emanuel R. Piore Award Recipients" (PDF) . IEEE . Архивировано из оригинала (PDF) 24 ноября 2010 г. . Получено 20 марта 2021 г. .
11. "ACM/IEEE A. Richard Newton Technical Impact Award in Electronic Design Automation". SIGDA . Получено 2 февраля 2018 г.