Роберт Шостак
Роберт Э. Шостак | |
|---|---|
 | |
| Рожденный | 26 июля 1948 г. |
| Альма-матер | AB, AM, доктор философии. Гарвард |
| Известный | |
| Награды | |
| Научная карьера | |
| Поля | Информатика |
Роберт Элиот Шостак (родился 26 июля 1948 года в Арлингтоне, штат Вирджиния) — американский ученый-компьютерщик и предприниматель из Кремниевой долины. В академической сфере он наиболее известен своей плодотворной работой в области распределенных вычислений, известной как византийская отказоустойчивость . Он также известен как соавтор базы данных Paradox , а совсем недавно — как основатель Vocera Communications, компании, которая производит носимые «Звездного пути» в стиле коммуникационные значки .
Шостак является автором более сорока научных статей и патентов, а также был редактором 7-й конференции по автоматизированному дедукции . он получил второе место по Эрдешу Благодаря сотрудничеству с Кеннетом Куненом . [1] Шостак получил премию Торальфа Скулема за «Решение комбинации теорий». [2]
Шостак — брат Сета Шостака , старшего астронома Института SETI и часто появляющегося на телевидении и радио.
Образование
[ редактировать ]Роберт Шостак родился в Арлингтоне, штат Вирджиния , в семье Артура и Берты Шостак (урожденная Гортенбург); его отец был инженером-электриком. [3] Он изучал математику и информатику в Гарвардском колледже , который окончил в 1970 году с отличием. В рамках своей дипломной работы он спроектировал и построил один из первых персональных компьютеров, использующих дискретную RTL логику ( микропроцессоры еще не были доступны) и память на магнитных сердечниках . [4] Он продолжил обучение в Гарварде, чтобы получить степень AM и доктора философии. получил степень бакалавра компьютерных наук в 1974 году. Во время учебы в Гарварде он был удостоен книжной премии Детура и стипендий от IBM и Национального научного фонда .
Карьера
[ редактировать ]После этого Шостак присоединился к исследовательскому персоналу в Лаборатории компьютерных наук (CSL) SRI International (бывший Стэнфордский исследовательский институт) в Менло-Парке, Калифорния . Большая часть его работы там была сосредоточена на автоматизированном доказательстве теорем и, в частности, на разработке процедур принятия решений. алгоритмов [5] [6] [7] [8] [9] для механизированного доказательства математических формул, которые часто встречаются при формальной проверке правильности компьютерных программ. [10]
В сотрудничестве с Ричардом Л. Шварцем из CSL и П. Майклом Меллиар-Смитом Шостак реализовал полуавтоматическое средство доказательства теорем, включающее некоторые из этих процедур принятия решений. [11] Средство доказательства использовалось для проверки свойств правильности абстрактной спецификации операционной системы SIFT (для программно-реализованной отказоустойчивости) и позже было включено в систему проверки прототипов SRI . Работа опубликована в статье SIFT: Проектирование и анализ отказоустойчивого компьютера для управления самолетом. [12] Эта статья была удостоена премии Жан-Клода Лапри 2014 года в области надежных вычислений. [13] установлен подгруппой 10.4 ИФИП по надежным вычислениям .
Интерактивная согласованность и византийская отказоустойчивость
[ редактировать ]Возможно, наиболее заметным академическим вкладом Шостака является создание отрасли распределенных вычислений, известной как византийская отказоустойчивость , также называемая интерактивной согласованностью .
Эта работа также проводилась в рамках проекта SIFT в НИИ. SIFT был задуман Джоном Х. Уэнсли, который предложил использовать сеть компьютеров общего назначения для надежного управления самолетом, даже если некоторые из этих компьютеров были неисправны. Компьютеры будут обмениваться сообщениями о текущем времени и состоянии самолета (каждый будет иметь свои собственные датчики и часы) и тем самым придут к консенсусу.
Вначале было неизвестно, сколько компьютеров потребуется для достижения консенсуса, если некоторые из них окажутся неисправными и, возможно, будут действовать «злонамеренно» для того, чтобы помешать консенсусу. Шостак формализовал проблему математически и доказал, что для 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. Компанию финансировал Бен Розен из Севина Розена . Ее продукт, база данных для ПК под названием Paradox , был выпущен в 1985 году и стал одним из первых продуктов баз данных, работавших на персональных компьютерах IBM . Его пользовательский интерфейс был основан на Query by example , графическом методе формулирования запросов, который был задуман Моше Злуфом из Исследовательского центра IBM Watson . В сентябре 1987 года Ansa Software была приобретена компанией Borland International , которая впоследствии выпустила несколько версий Windows. Сообщество пользователей все еще существует спустя более тридцати лет. На момент написания этой статьи сторонняя версия DOS все еще доступна для 64-битной Windows .
Шостак также является основателем компании Vocera Communications , которую он основал в марте 2000 года. Продукт, который облегчает общение между членами команд в больницах и других предприятиях без помощи рук, включает в себя носимые значки с голосовой поддержкой, очень похожие на коммуникационные значки Star Trek . [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 г., выдан в июне 1016 г., передан 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.
Ссылки
[ редактировать ]- ^ WW Бледсо; Кеннет Кунен ; Роберт Э. Шостак (1985). «Результаты полноты для средств доказательства неравенства». Искусственный интеллект . 27 (3): 255–288. дои : 10.1016/0004-3702(85)90015-3 .
- ^ «Сколемская премия» . cadeinc.org . Проверено 6 декабря 2023 г.
- ^ «Федеральная перепись населения США 1950 года» . Ancestry.com . Проверено 12 июля 2022 г.
- ^ Шостак, Роберт (1970). «НИЦ: небольшой недорогой цифровой компьютер» .
- ^ Роберт Э. Шостак (1977). «О методе SUP-INF доказательства формул Пресбургера» . Журнал АКМ . 24 (4): 529–543. дои : 10.1145/322033.322034 . S2CID 16778115 .
- ^ Роберт Э. Шостак (1978). «Алгоритм рассуждений о равенстве» . Коммуникации АКМ . 21 (7): 583–585. дои : 10.1145/359545.359570 . S2CID 1036470 .
- ^ Роберт Э. Шостак (1979). «Процедура практического решения арифметических операций с функциональными символами» . Журнал АКМ . 26 (2): 351–360. дои : 10.1145/322123.322137 . S2CID 13502248 .
- ^ Роберт Э. Шостак (1981). «Решение линейных неравенств путем вычисления остатков цикла». Журнал АКМ . 28 (4): 351–360.
- ^ Роберт Э. Шостак (1984). «Решение комбинации теорий» . Журнал АКМ . 31 (1): 1–12. дои : 10.1145/2422.322411 . S2CID 5541114 .
- ^ А., Маккензи, Дональд (2001). Механизация доказательства: вычисления, риск и доверие . Кембридж, Массачусетс: MIT Press. стр. 268–272 . ISBN 978-0262133937 . OCLC 45835532 .
{{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка ) - ^ Шостак, Роберт Э.; Шостак, Ричард Л.; Меллиар-Смит, П. Майкл (1982). «STP: механизированная логика для спецификации и проверки». В Лавленде, Дональд (ред.). Материалы 6-й конференции по автоматизированному дедукции . Конспекты лекций по информатике. Том. 138. Шпрингер, Берлин, Гейдельберг. стр. 32–49. дои : 10.1007/BFb0000050 . ISBN 3-540-11558-7 .
- ^ Уэнсли, Джон Х.; Лэмпорт, Л.; Голдберг, Дж.; Грин, МВт; Левитт, КНЦ; Меллиар-Смит, премьер-министр; Шостак, Р.Э.; Вайншток, CB (октябрь 1978 г.). «SIFT: Проектирование и анализ отказоустойчивого компьютера управления самолетом». Труды IEEE . 66 (10): 1240–1255. дои : 10.1109/PROC.1978.11114 . S2CID 4020660 .
- ^ Перейти обратно: а б «Премия Жан-Клода Лапри» . jclaprie-award.dependentability.org . Проверено 21 февраля 2019 г.
- ^ М. Пиз; Р. Шостак; Л. Лэмпорт (1979). «Достижение соглашения при наличии разногласий». Журнал АКМ . 27 (2): 228–234. CiteSeerX 10.1.1.68.4044 . дои : 10.1145/322186.322188 . S2CID 6429068 .
- ^ Л. Лэмпорт; Р. Шостак; М. Пиз (1982). «Проблема византийских генералов». Транзакции ACM в языках и системах программирования . 4 (1): 382–401. CiteSeerX 10.1.1.64.2312 . дои : 10.1145/357172.357176 . S2CID 55899582 .
- ^ Имран, Башир (17 марта 2017 г.). Освоение блокчейна: объяснение распределенных реестров, децентрализации и смарт-контрактов . Бирмингем, Великобритания. стр. 12, 30. ISBN. 9781787129290 . OCLC 981928401 .
{{cite book}}: CS1 maint: отсутствует местоположение издателя ( ссылка ) - ^ Хессельдал, Арик (16 марта 2004 г.). «Ваш Trekkie Communicator готов» . Журнал Форбс .
- ^ Галлахер, Дэн (28 марта 2012 г.). «Vocera Communications готовится к IPO» . МаркетВотч .
| Международный | |
|---|---|
| Национальный | |
| Другой | |
