Дэвид Л. Дилл

Дэвид Л. Дилл
Дэвид Л. Дилл
Рожденный	8 января 1957 г. (67 лет)
Национальность	Соединенные Штаты
Альма-матер	Массачусетский технологический институт
Награды	Премия Алонзо Чёрча ; КАВ Премия ; Премия EFF «Пионер» ;
	Научная карьера
Докторантура	Эдмунд М. Кларк
Известные студенты	Раджив Алур
Веб-сайт	[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. Он работал в Meta с 2018 по 2023 год в качестве ведущего исследователя блокчейн-проекта Libra/Diem.

Работа

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

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

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

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

Дилл членом ACM является и IEEE . Его диссертация была удостоена награды ACM «Выдающаяся диссертация» в 1988 году, и в том же году он был назван президентом молодым исследователем . Он получил награды за лучшие статьи на Международной конференции IEEE по компьютерному дизайну в 1991 году и на конференции по автоматизации проектирования в 1993 и 1998 годах. В 2004 году он получил премию Electronic Frontier Foundation Pioneer Award за руководство и поддержку популярного движения за целостность и прозрачность в современном мире. выборы. В 2008 году он и Раджив Алур получили награду «Компьютерная верификация» за фундаментальный вклад в теорию верификации систем реального времени . В 2010 году он получил две награды «Проверка временем» на конференции «Логика в компьютерных науках» (за статьи, опубликованные в LICS в 1990 году). В 2013 году он был избран членом Национальной инженерной академии и Американской академии искусств и наук . В 2016 году он и Раджив Алур получили Премию Алонзо Чёрча за выдающийся вклад в логику от Специальная группа по интересам ACM по логике и вычислениям (SIGLOG) , Европейская ассоциация теоретической информатики (EATCS), Европейская ассоциация логики компьютерных наук (EACSL) и Общество Курта Гёделя (KGS). Также в 2016 году он получил награду «Испытание временем» на конференции ACM по компьютерной и коммуникационной безопасности. В 2021 году он был одним из группы исследователей, получивших награду за компьютерную верификацию за новаторский вклад в основы теории и практики теорий выполнимости по модулю (SMT). Он и его соавторы также получили награду «Испытание временем» на конференции «Логика в компьютерных науках» в 2021 году.

Ссылки

^ Jump up to: ^а ^б «Дэвид Л. Дилл» . Архивировано из оригинала 17 сентября 2017 года . Проверено 12 сентября 2017 г.
^ Дэвид Л. Дилл. 1989, Теория трассировки для автоматической иерархической проверки схем, независимых от скорости. Архивировано 25 мая 2019 г. в Wayback Machine . МТИ Пресс .
^ Дж. Р. Берч, Э. М. Кларк, К. Л. Макмиллан, Д. Л. Дилл, Л. Дж. Хван. 1990, Проверка символьной модели: 10 ²⁰ Штаты и за их пределами . В Proceedings of Logic in Computer Science (LIICS '90), 428–439.
^ Дэвид Л. Дилл, Андреас Дж. Дрекслер, Алан Дж. Ху и К. Хан Ян. Проверка протокола как средство проектирования аппаратного обеспечения. Архивировано 19 сентября 2015 г. на Wayback Machine . Компьютерный дизайн: СБИС в компьютерах и процессорах, 1992. ICCD'92.
^ Дэвид Л. Дилл, Ретроспектива Мерфи , 25 лет проверки моделей, 2008. LNCS, Springer.
^ Раджив Алур, Дэвид Л. Дилл. 1994, Теория временных автоматов . Теоретическая информатика, том 126, выпуск 2, 183–235.
^ Берч, Джерри Р.; Дилл, Дэвид Л. (1994). «Автоматическая проверка конвейерного микропроцессорного управления». Компьютерная проверка . Конспекты лекций по информатике. Том. 818. стр. 68–80. дои : 10.1007/3-540-58179-0_44 . ISBN 978-3-540-58179-6 .
^ К. Барретт, Д. Дилл, Дж. Левитт. 1996, Проверка достоверности комбинаций теорий равенства . В Трудах по формальным методам автоматизированного проектирования (FMCAD '96), 187-201.
^ Стамп, Аарон; Барретт, Кларк В.; Дилл, Дэвид Л. (2002). «CVC: Совместная проверка действительности». Компьютерная проверка . Конспекты лекций по информатике. Том. 2404. стр. 500–504. CiteSeerX 10.1.1.17.1530 . дои : 10.1007/3-540-45657-0_40 . ISBN 978-3-540-43997-4 . S2CID 26802227 .
^ Ганеш, Виджай; Дилл, Дэвид Л. (2007). «Процедура принятия решения для битовых векторов и массивов». Компьютерная проверка . Конспекты лекций по информатике. Том. 4590. стр. 519–531. CiteSeerX 10.1.1.144.5247 . дои : 10.1007/978-3-540-73368-3_52 . ISBN 978-3-540-73367-6 .
^ К. Кадар, В. Ганеш, П.М. Павловский, Д.Л. Дилл и Д.Р. Энглер. 2008, EXE: Автоматическое создание входных данных транзакций Death ACM по информационной и системной безопасности (TISSEC), Vol. 12, Выпуск 2, 10:1-10:38.
^ «Постановление об электронном голосовании» . Проверено 12 сентября 2017 г.
^ «Подтвержденное голосование» . Архивировано из оригинала 5 октября 2017 года . Проверено 12 сентября 2017 г.

Внешние ссылки

[DillWebsite-1] Jump up to: ^а ^б «Дэвид Л. Дилл» . Архивировано из оригинала 17 сентября 2017 года . Проверено 12 сентября 2017 г.

[2] Дэвид Л. Дилл. 1989, Теория трассировки для автоматической иерархической проверки схем, независимых от скорости. Архивировано 25 мая 2019 г. в Wayback Machine . МТИ Пресс .

[3] Дж. Р. Берч, Э. М. Кларк, К. Л. Макмиллан, Д. Л. Дилл, Л. Дж. Хван. 1990, Проверка символьной модели: 10 ²⁰ Штаты и за их пределами . В Proceedings of Logic in Computer Science (LIICS '90), 428–439.

[4] Дэвид Л. Дилл, Андреас Дж. Дрекслер, Алан Дж. Ху и К. Хан Ян. Проверка протокола как средство проектирования аппаратного обеспечения. Архивировано 19 сентября 2015 г. на Wayback Machine . Компьютерный дизайн: СБИС в компьютерах и процессорах, 1992. ICCD'92.

[5] Дэвид Л. Дилл, Ретроспектива Мерфи , 25 лет проверки моделей, 2008. LNCS, Springer.

[6] Раджив Алур, Дэвид Л. Дилл. 1994, Теория временных автоматов . Теоретическая информатика, том 126, выпуск 2, 183–235.

[7] Берч, Джерри Р.; Дилл, Дэвид Л. (1994). «Автоматическая проверка конвейерного микропроцессорного управления». Компьютерная проверка . Конспекты лекций по информатике. Том. 818. стр. 68–80. дои : 10.1007/3-540-58179-0_44 . ISBN 978-3-540-58179-6 .

[8] К. Барретт, Д. Дилл, Дж. Левитт. 1996, Проверка достоверности комбинаций теорий равенства . В Трудах по формальным методам автоматизированного проектирования (FMCAD '96), 187-201.

[9] Стамп, Аарон; Барретт, Кларк В.; Дилл, Дэвид Л. (2002). «CVC: Совместная проверка действительности». Компьютерная проверка . Конспекты лекций по информатике. Том. 2404. стр. 500–504. CiteSeerX 10.1.1.17.1530 . дои : 10.1007/3-540-45657-0_40 . ISBN 978-3-540-43997-4 . S2CID 26802227 .

[10] Ганеш, Виджай; Дилл, Дэвид Л. (2007). «Процедура принятия решения для битовых векторов и массивов». Компьютерная проверка . Конспекты лекций по информатике. Том. 4590. стр. 519–531. CiteSeerX 10.1.1.144.5247 . дои : 10.1007/978-3-540-73368-3_52 . ISBN 978-3-540-73367-6 .

[11] К. Кадар, В. Ганеш, П.М. Павловский, Д.Л. Дилл и Д.Р. Энглер. 2008, EXE: Автоматическое создание входных данных транзакций Death ACM по информационной и системной безопасности (TISSEC), Vol. 12, Выпуск 2, 10:1-10:38.

[12] «Постановление об электронном голосовании» . Проверено 12 сентября 2017 г.

[13] «Подтвержденное голосование» . Архивировано из оригинала 5 октября 2017 года . Проверено 12 сентября 2017 г.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]

Базы данных авторитетного контроля
Международный	БЫСТРЫЙ ЯВЛЯЮТСЯ ВИАФ WorldCat
Национальный	Израиль Соединенные Штаты
академики	Ассоциация вычислительной техники ДБЛП Google Академика MathSciNet Проект математической генеалогии
Другой	ИдРеф