Дэвид Л. Дилл
Американский учёный-компьютерщик
Дэвид Л. Дилл
Рожденный( 1957-01-08 )8 января 1957 г. (67 лет)
Национальность Соединенные Штаты
Альма-матерМассачусетский технологический институт
Награды
Научная карьера
научный руководительЭдмунд М. Кларк
Известные студентыРаджив Алур
Веб-сайт[1]

Дэвид Лансинг Дилл (родился 8 января 1957 года) — учёный-компьютерщик и учёный, известный своим вкладом в формальную верификацию , безопасность электронного голосования и биологию вычислительных систем .

В 2013 году Дилл был избран членом Национальной инженерной академии за разработку методов проверки оборудования, программного обеспечения и систем электронного голосования.

Он является почетным профессором имени Дональда Э. Кнута в Школе инженерии и почетным профессором компьютерных наук в Стэнфордском университете .

Биография

Дилл получил степень бакалавра наук в области компьютерных наук и электротехники в Массачусетском технологическом институте , Кембридж, Массачусетс , в 1979 году, степень магистра наук в области компьютерных наук в Университете Карнеги-Меллона , Питтсбург, Пенсильвания , в 1982 году и степень доктора философии в области компьютерных наук в 1987 году, также в Университете Карнеги-Меллона . После получения степени доктора философии он присоединился к преподавательскому составу кафедры компьютерных наук в Стэнфордском университете , Стэнфорд, Калифорния . [1] Он стал доцентом в 1994 году и полным профессором в 2000 году. В 2016 году он стал первым получателем профессорской должности Дональда Э. Кнута , пожертвованной кафедры в Школе инженерии Стэнфордского университета . С июля 1995 по сентябрь 1996 года он был главным научным сотрудником в 0-In Design Automation (приобретенной Mentor Graphics в 2004 году), а с 2016 по 2017 год он был главным научным сотрудником в LocusPoint Networks, LLC. С 2018 по 2023 год он работал в Meta в качестве ведущего исследователя по проекту блокчейна Libra/Diem.

Работа

Интересы Дилла включают проектирование асинхронных схем , проверку программного и аппаратного обеспечения , автоматическое доказательство теорем , безопасность электронного голосования и биологию вычислительных систем . Его докторская диссертация стала важным вкладом в проверку асинхронных схем и была опубликована издательством MIT Press в 1989 году. [2] Он внес вклад в разработку символической проверки моделей , помогая улучшить масштабируемость этой техники. [3] Вскоре после прибытия в Стэнфорд Дилл и его студенты разработали верификатор конечных состояний Мерфи, который позже использовался для проверки протоколов когерентности кэша в мультипроцессорах и ЦП нескольких крупных производителей компьютеров. [4] [5] Он и Раджив Алур расширили классическую теорию автоматов с помощью часов с действительными значениями, изобретя синхронизированные автоматы . [6] В 1994 году он и Джерри Берч опубликовали влиятельную статью о проверке микропроцессоров , изобретя метод, известный как метод проверки Берча-Дилла. [7] Он также был одним из первых, кто внес вклад в область исследований, известную как теории выполнимости по модулю (SMT), руководя разработкой нескольких ранних решателей SMT: Stanford Validity Checker (SVC), [8] Cooperating Validity Checker ( CVC ), [9] и Simple Theorem Prover ( STP ). [10] И он внес вклад в разработку ключевого приложения решателей SMT для тестирования программного обеспечения, известного как concolic testing . [11]

Электронное голосование

В январе 2003 года Дилл стал автором «Резолюции об электронном голосовании» [12] , которая призывает к проверяемому избирателем аудиторскому следу на всем избирательном оборудовании. Резолюция была одобрена тысячами людей, включая экспертов по компьютерам и безопасности и выборных должностных лиц. В июле того же года он создал VerifiedVoting.org, а в феврале 2004 года он основал Verified Voting Foundation , в совете директоров которого он остается. В мае 2004 года он дал несколько интервью СМИ на эту тему, в том числе с Лу Доббсом Tonight и Джимом Лерером . В апреле 2005 года он дал показания перед Комиссией по реформе федеральных выборов , сопредседателями которой были Джимми Картер и Джеймс Бейкер , а в июне он дал показания перед Сенатом Соединенных Штатов . [1] [13]

Профессиональное признание

Дилл является членом ACM и IEEE . Его диссертация получила премию ACM Distinguished Dissertation в 1988 году, и в том же году он был назван Президентским молодым исследователем . Он получил награды за лучшую статью на Международной конференции IEEE по компьютерному дизайну в 1991 году и на Конференции по автоматизации проектирования в 1993 и 1998 годах. Он получил премию Electronic Frontier Foundation Pioneer Award в 2004 году за руководство и развитие популярного движения за честность и прозрачность современных выборов. В 2008 году он и Раджив Алур получили премию Computer Aided Verification за фундаментальный вклад в теорию верификации систем реального времени . В 2010 году он получил две награды test of time от конференции Logic in Computer Science (за статьи, опубликованные в LICS в 1990 году). В 2013 году он был избран в Национальную инженерную академию и Американскую академию искусств и наук . В 2016 году он и Раджив Алур получили премию Алонзо Чёрча за выдающийся вклад в логику от ACM Special Interest Group for Logic and Computation (SIGLOG) , Европейской ассоциации теоретической компьютерной науки (EATCS), Европейской ассоциации логики компьютерных наук (EACSL) и Общества Курта Гёделя (KGS). Также в 2016 году он получил премию «Испытание временем» от конференции ACM по компьютерной и коммуникационной безопасности. В 2021 году он был одним из группы исследователей, получивших премию Computer Aided Verification за новаторский вклад в основы теории и практики теорий выполнимости по модулю (SMT). Он и его соавторы также получили премию Test of Time от конференции Logic in Computer Science в 2021 году. В 2024 году он получил третью премию Computer Aided Verification с группой исследователей за алгоритм ReluPlex для проверки глубоких нейронных сетей.

Ссылки

  1. ^ ab "David L. Dill". Архивировано из оригинала 17 сентября 2017 г. Получено 12 сентября 2017 г.
  2. ^ Дэвид Л. Дилл. 1989, Теория трассировки для автоматической иерархической проверки скоростно-независимых цепей. Архивировано 25 мая 2019 г. в Wayback Machine . MIT Press .
  3. ^ JR Burch, EM Clarke, KL McMillan, DL Dill, LJ Hwang. 1990, Проверка символической модели: 1020 состояний и далее. В Proceedings of Logic in Computer Science (LICS '90), 428-439.
  4. ^ Дэвид Л. Дилл, Андреас Дж. Дрекслер, Алан Дж. Ху и К. Хань Янг Проверка протокола как средство разработки оборудования Архивировано 19 сентября 2015 г. на Wayback Machine . Проектирование компьютеров: СБИС в компьютерах и процессорах, 1992. ICCD'92.
  5. ^ Дэвид Л. Дилл, Ретроспектива Мерфи, 25 лет проверки моделей, 2008. LNCS, Springer
  6. ^ Раджив Алур, Дэвид Л. Дилл. 1994, Теория синхронизированных автоматов. Теоретическая информатика, том 126, выпуск 2, 183-235.
  7. ^ Берч, Джерри Р.; Дилл, Дэвид Л. (1994). «Автоматическая проверка конвейерного микропроцессорного управления». Computer Aided Verification . Lecture Notes in Computer Science. Vol. 818. pp. 68–80. doi :10.1007/3-540-58179-0_44. ISBN 978-3-540-58179-6.
  8. ^ C. Barrett, D. Dill, J. Levitt. 1996, Проверка валидности комбинаций теорий с равенством. В Трудах по формальным методам в автоматизированном проектировании (FMCAD '96), 187-201.
  9. ^ Стамп, Аарон; Барретт, Кларк В.; Дилл, Дэвид Л. (2002). "CVC: кооперативная проверка достоверности". Computer Aided Verification . Lecture Notes in Computer Science. Vol. 2404. pp. 500–504. CiteSeerX 10.1.1.17.1530 . doi :10.1007/3-540-45657-0_40. ISBN  978-3-540-43997-4. S2CID  26802227.
  10. ^ Ганеш, Виджай; Дилл, Дэвид Л. (2007). «Процедура принятия решений для битовых векторов и массивов». Computer Aided Verification . Lecture Notes in Computer Science. Vol. 4590. pp. 519–531. CiteSeerX 10.1.1.144.5247 . doi :10.1007/978-3-540-73368-3_52. ISBN  978-3-540-73367-6.
  11. ^ C. Cadar, V. Ganesh, PM Pawlowski, DL Dill и DR Engler. 2008, EXE: Автоматическое создание входных данных транзакций Death ACM по безопасности информации и систем (TISSEC), том 12, выпуск 2, 10:1-10:38.
  12. ^ "Резолюция об электронном голосовании" . Получено 12 сентября 2017 г.
  13. ^ "Проверенное голосование". Архивировано из оригинала 5 октября 2017 г. Получено 12 сентября 2017 г.
Взято с "https://en.wikipedia.org/w/index.php?title=David_L._Dill&oldid=1256648008"