Роберт Шостак
Американский учёный-компьютерщик
Роберт Э. Шостак
Рожденный( 1948-07-26 )26 июля 1948 г. (76 лет)
Округ Арлингтон, Вирджиния , США
Альма-матерAB, AM, Ph.D. Гарвард
Известный
Награды
Научная карьера
ПоляИнформатика

Роберт Элиот Шостак (родился 26 июля 1948 года в Арлингтоне, Вирджиния) — американский учёный-компьютерщик и предприниматель из Кремниевой долины. Он наиболее известен в академическом плане своей основополагающей работой в области распределённых вычислений, известной как Byzantine Fault Tolerance . Он также известен как соавтор Paradox Database и, совсем недавно, как основатель Vocera Communications, компании, которая производит носимые коммуникационные значки , похожие на Star Trek .

Шостак является автором более сорока научных статей и патентов, а также был редактором 7-й конференции по автоматизированной дедукции . Он имеет номер Эрдёша 2 благодаря сотрудничеству с Кеннетом Куненом . [1] Шостак получил премию Торальфа Сколема за «Решающие комбинации теорий» [2]

Шостак — брат Сета Шостака , старшего астронома в Институте SETI , который часто выступает на телевидении и радио.

Образование

Роберт Шостак родился в Арлингтоне, штат Вирджиния , в семье Артура и Берты Шостак (урожденной Гортенбург); его отец был инженером-электриком. [3] Он изучал математику и информатику в Гарвардском колледже , который окончил в 1970 году с отличием. В рамках своей дипломной работы он спроектировал и построил один из первых персональных компьютеров, используя дискретную RTL- логику ( микропроцессоры тогда еще не были доступны) и память на магнитных сердечниках . [4] Он продолжил обучение в Гарварде, чтобы получить степень AM и степень доктора философии в области компьютерных наук в 1974 году. Во время учебы в Гарварде он был награжден премией Detur Book Prize и стипендиями от IBM и Национального научного фонда .

Карьера

После этого Шостак присоединился к исследовательскому составу в Computer Science Lab (CSL) в SRI International (ранее Стэнфордский исследовательский институт) в Менло-Парке, Калифорния . Большая часть его работы там была сосредоточена на автоматизированном доказательстве теорем и, в частности, на разработке алгоритмов процедуры принятия решений [5] [6] [7] [8] [9] для механизированного доказательства видов математических формул, которые часто встречаются при формальной проверке корректности компьютерных программ. [10]

В сотрудничестве с Ричардом Л. Шварцем и П. Майклом Меллиар-Смитом из CSL Шостак реализовал полуавтоматическую доказательную машину теорем, включающую некоторые из этих процедур принятия решений. [11] Доказательная машина использовалась для проверки свойств корректности абстрактной спецификации операционной системы SIFT (Software Implemented Fault Tolerance) и позже была включена в систему проверки прототипов SRI . Работа была опубликована в статье SIFT: Design and analysis of a fault-tolerant computer for aircraft control [12] Эта статья была удостоена премии Жана-Клода Лапри 2014 года в области надежных вычислений [13], учрежденной подгруппой IFIP 10.4 по надежным вычислениям .

Интерактивная согласованность и византийская отказоустойчивость

Возможно, наиболее значимым академическим вкладом Шостака является создание направления распределенных вычислений, известного как византийская отказоустойчивость , также называемая интерактивной согласованностью .

Эта работа также проводилась в связи с проектом SIFT в SRI. SIFT был задуман Джоном Х. Уэнсли, который предложил использовать сеть компьютеров общего назначения для надежного управления самолетом, даже если некоторые из этих компьютеров были неисправны. Компьютеры обменивались бы сообщениями о текущем времени и состоянии самолета (каждый имел бы свои собственные датчики и часы) и таким образом достигали бы консенсуса.

Вначале было неизвестно, сколько компьютеров потребуется для достижения консенсуса, если некоторые n из них неисправны и, возможно, действуют «злонамеренно», чтобы помешать консенсусу. Шостак формализовал задачу математически и доказал, что для n неисправных компьютеров для любого алгоритма, который мог бы гарантировать консенсус, или того, что он назвал интерактивной согласованностью , необходимо не менее 3 n +1 компьютеров . Он также разработал алгоритм для n = 1, доказав, что четырех компьютеров достаточно, используя два раунда передачи сообщений. Затем его коллега Маршалл Пиз обобщил результат, построив алгоритм для 3 n +1 компьютеров, который работает для всех n > 0, тем самым показав, что 3 n +1 достаточно, а также необходимо.

Позже в CSL присоединился Лесли Лэмпорт , который показал, что если сообщения можно подписывать цифровой подписью, то для этого потребуется всего 3 n .

Совместные результаты были опубликованы в 1979 году в основополагающей статье « Достижение согласия при наличии неисправностей » [14] , которая была удостоена премии Эдсгера В. Дейкстры 2005 года в области распределенных вычислений, а также премии Жана-Клода Лапри 2013 года [13].

Те же авторы помогли популяризировать проблему интерактивной согласованности в своей статье 1982 года «Проблема византийских генералов» [ 15] , которая представляет ее в форме красочной аллегории, предложенной Лэмпортом. В аллегории компьютеры заменяются византийскими генералами, которым необходимо координировать время атаки на врага, обмениваясь сообщениями, доставляемыми курьерами. (Первоначальная формулировка включала албанских, а не византийских генералов, но Джек Голдберг, глава CSL, предположил, что это можно интерпретировать как то, что сейчас можно назвать культурной апроприацией , поэтому название было изменено на византийское по теории, что это может быть менее вероятно, чтобы вызвать оскорбление.)

Работа над византийским соглашением породила целую подобласть распределенных вычислений с сотнями опубликованных статей, исследующих расширения и приложения исходных результатов. Одна из самых интересных из них — реализация блокчейнов , в которой интерактивная согласованность ищется среди распределенной сети компьютеров. [16] Блокчейны поддерживают целостность криптовалют, таких как биткойн .

Предпринимательские начинания

В 1984 году Шостак и его коллега Ричард Шварц основали в Кремниевой долине стартап под названием Ansa Software. Компанию финансировал Бен Розен из Sevin Rosen . Ее продукт, база данных для ПК под названием Paradox , был запущен в 1985 году и был одним из первых продуктов баз данных, работающих на персональных компьютерах IBM . Ее пользовательский интерфейс был основан на Query by Example , графическом методе формулирования запросов, который был задуман Моше Злуфом в исследовательском центре IBM Watson . В сентябре 1987 года Ansa Software была куплена Borland International , которая впоследствии выпустила несколько версий Windows. Сообщество пользователей все еще существует спустя более тридцати лет. На момент написания этой статьи сторонняя версия DOS все еще доступна для 64-разрядной Windows .

Шостак также является основателем Vocera Communications, которую он запустил в марте 2000 года. Продукт, который обеспечивает беспроводную связь между членами команд в больницах и других предприятиях, представляет собой носимые значки с функцией голосового управления, очень похожие на значки Star Trek Communication . [17] Компания стала публичной в 2012 году (NYSE:VCRA) [18] и имеет рыночную капитализацию около $1 млрд на момент написания этой статьи. Шостак занимал должность технического директора и главного архитектора до выхода на пенсию в 2013 году и был членом совета директоров до IPO компании.

Избранные патенты

  • Патент США 5,694,608 «Немодальная система базы данных с методами инкрементального обслуживания живых представлений» , подан в январе 1995 г., выдан в декабре 1997 г., передан Borland International, Inc.
  • Патент США 5,913,029 «Распределенная база данных и метод» , подан в апреле 1957 г., выдан в июне 1999 г., передан Portera Systems
  • Патент США 6,892,083 «Система и метод беспроводной связи с голосовым управлением» , подан в августе 2001 г., выдан в мае 2005 г., передан Vocera Communications, Inc.
  • Патент США 7,190,802 «Корпус микрофона для снижения акустических помех» , подан в августе 2002 г., выдан в марте 2007 г., передан Vocera Communications, Inc.
  • Патент США 7,206,594 «Система и метод беспроводной чат-комнаты связи» , подан в феврале 2004 г., выдан в апреле 2007 г., передан Vocera Communications, Inc.
  • Патент США 7,248,881 «Система и способ голосовой связи с устройством доступа или приложением для пропуска» , подан в феврале 2008 г., выдан в июне 1916 г., передан Vocera Communications, Inc.
  • Патент США 7,310,541 «Система и метод голосовой связи» , подан в марте 2005 г., выдан в декабре 2007 г., передан Vocera Communications, Inc.
  • Патент США 7,457,751 «Система и метод повышения точности распознавания в приложениях распознавания речи» , подан в ноябре 2004 г., выдан в ноябре 2008 г., передан Vocera Communications, Inc.
  • Патент США 7,764,972 «Система и метод чата на основе гетерогенных устройств» , подан в феврале 2007 г., выдан в июле 2010 г., передан Vocera Communications, Inc.
  • Патент США 7,953,447 « Система голосового управления связью и способ с использованием значка» , заявка подана в феврале 2007 г., выдана в мае 2011 г., передана Vocera Communications, Inc.
  • Патент США 8,098,806 «Неспецифическая для пользователя система и метод беспроводной связи» , подан в августе 2003 г., выдан в январе 2012 г., передан Vocera Communications, Inc.
  • Патент США 8,175,887 « Система и метод повышения точности распознавания в приложениях распознавания речи» , подан в октябре 2008 г., выдан в мае 2012 г., передан Vocera Communications, Inc.
  • Патент США 8,498,865 «Система и метод распознавания речи с использованием статистики групповых вызовов» , подан в феврале 2011 г., выдан в июле 2013 г., передан Vocera Communications, Inc.
  • Патент США 8,626,246 «Система беспроводной связи с голосовым управлением и способ с использованием значка» , заявка подана в мае 2011 г., выдана в январе 2014 г., передана Vocera Communications, Inc.
  • Патент США 9,817,809 «Система и метод обработки омонимов в системе распознавания речи» , подан в феврале 2009 г., выдан в ноябре 2017 г., передан Vocera Communications, Inc.

Ссылки

  1. ^ WW Bledsoe; Kenneth Kunen ; Robert E. Shostak (1985). «Результаты полноты для доказательств неравенства». Искусственный интеллект . 27 (3): 255– 288. doi :10.1016/0004-3702(85)90015-3.
  2. ^ "Премия Сколема". cadeinc.org . Проверено 6 декабря 2023 г.
  3. ^ "Федеральная перепись населения США 1950 года". Ancestry.com . Получено 12 июля 2022 г. .
  4. ^ Шостак, Роберт (1970). «SIC: небольшой недорогой цифровой компьютер».
  5. ^ Роберт Э. Шостак (1977). «О методе SUP-INF для доказательства формул Пресбургера». Журнал ACM . 24 (4): 529– 543. doi : 10.1145/322033.322034 . S2CID  16778115.
  6. ^ Роберт Э. Шостак (1978). «Алгоритм для рассуждений о равенстве». Сообщения ACM . 21 (7): 583– 585. doi : 10.1145/359545.359570 . S2CID  1036470.
  7. ^ Роберт Э. Шостак (1979). «Практическая процедура принятия решений для арифметики с функциональными символами». Журнал ACM . 26 (2): 351– 360. doi : 10.1145/322123.322137 . S2CID  13502248.
  8. ^ Роберт Э. Шостак (1981). «Решение линейных неравенств путем вычисления вычетов циклов». Журнал ACM . 28 (4): 351–360 .
  9. ^ Роберт Э. Шостак (1984). «Решающие комбинации теорий». Журнал ACM . 31 (1): 1– 12. doi : 10.1145/2422.322411 . S2CID  5541114.
  10. ^ А., Маккензи, Дональд (2001). Механизация доказательства: вычисления, риск и доверие. Кембридж, Массачусетс: MIT Press. С. 268–272. ISBN 978-0262133937. OCLC  45835532.{{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
  11. ^ Шостак, Роберт Э.; Шостак, Ричард Л.; Меллиар-Смит, П. Майкл (1982). "STP: Механизированная логика для спецификации и проверки". В Loveland, Дональд (ред.). Труды 6-й конференции по автоматизированной дедукции . Конспект лекций по информатике. Том 138. Springer, Берлин, Гейдельберг. стр.  32–49 . doi :10.1007/BFb0000050. ISBN 3-540-11558-7.
  12. ^ Уэнсли, Джон Х.; Лампорт, Л.; Голдберг, Дж.; Грин, М. В.; Левитт, К. Н.; Меллиар-Смит, П. М.; Шостак, Р. Э.; Вайншток, К. Б. (октябрь 1978 г.). «SIFT: Проектирование и анализ отказоустойчивого компьютера для управления самолетом». Труды IEEE . 66 (10): 1240– 1255. doi :10.1109/PROC.1978.11114. S2CID  4020660.
  13. ^ ab "Премия Жана-Клода Лапри". jclaprie-award.dependability.org . Получено 21.02.2019 .
  14. ^ М. Пиз; Р. Шостак; Л. Лампорт (1979). «Достижение соглашения при наличии разломов». Журнал ACM . 27 (2): 228– 234. CiteSeerX 10.1.1.68.4044 . doi :10.1145/322186.322188. S2CID  6429068. 
  15. ^ Л. Лампорт; Р. Шостак; М. Пиз (1982). «Проблема византийских генералов». Труды ACM по языкам и системам программирования . 4 (1): 382– 401. CiteSeerX 10.1.1.64.2312 . doi :10.1145/357172.357176. S2CID  55899582. 
  16. ^ Имран, Башир (2017-03-17). Освоение блокчейна: распределенные реестры, децентрализация и объяснение смарт-контрактов . Бирмингем, Великобритания. стр. 12, 30. ISBN 9781787129290. OCLC  981928401.{{cite book}}: CS1 maint: location missing publisher (link)
  17. ↑ Хессельдаль, Арик (16 марта 2004 г.). «Ваш Trekkie Communicator готов». Журнал Forbes .
  18. ^ Галлахер, Дэн (28 марта 2012 г.). «Vocera Communications совершает прыжок на дебютном IPO». MarketWatch .
Retrieved from "https://en.wikipedia.org/w/index.php?title=Robert_Shostak&oldid=1230382702"