Кеннет Л. Макмиллан

Кеннет Л. Макмиллан — американский учёный-компьютерщик, работающий в области формальных методов , логики и языков программирования . Он является профессором кафедры информатики Техасского университета в Остине , где он возглавляет адмирала Б. Р. Инмана . кафедру теории вычислений, посвященную столетнему юбилею [1]
Карьера [ править ]
Макмиллан получил докторскую степень. из Университета Карнеги-Меллон в 1992 году под руководством Эдмунда М. Кларка . [2] Ему приписывают изобретение символической проверки моделей во время его дипломной работы, которая принесла ему в 1992 году премию ACM Doctoral Dissertation Award , высшую премию за докторскую диссертацию, присуждаемую Ассоциацией вычислительной техники (ACM). [3] Он также выиграл премию ACM Paris Kanellakis 1998 года за теорию и практику совместно с Рэндалом Брайантом , Эдмундом Кларком и Э. Алленом Эмерсоном за работу по проверке символических моделей. [4] Макмиллан впоследствии работал в Bell Labs , Cadence Berkeley Labs и был главным научным сотрудником в Microsoft Research, Редмонд. [5] прежде чем поступить на факультет Техасского университета в Остине в 2021 году. [6]
Исследования [ править ]
Макмиллан стал пионером в нескольких влиятельных областях исследований формальных методов. Его первоначальная работа по проверке символических моделей на основе бинарных диаграмм решений завершилась созданием SMV/nuSMV семейства средств проверки моделей . [7] Он также стал пионером в методах, основанных на интерполяции Крейга , при проверке моделей систем с бесконечным состоянием. [8] Он также известен своей работой по решению условий ограниченного предложения Horn (CHC). [9] и инструмент проверки распределенной системы IVy. [10]
Награды [ править ]
- 2014 - POPL за самую влиятельную бумагу Премия [11]
- 2010 - Премия LICS «Испытание временем» [12]
- 1998 - Медаль КМУ Аллена Ньюэлла [13]
- 1998 - Премия КАВ [14]
- 1998 - Премия ACM Парижа Канеллакиса
- 1996 - SRC за техническое совершенство Премия [15]
- 1992 - Премия ACM за докторскую диссертацию
Сервис [ править ]
Макмиллан в настоящее время входит в состав руководящего комитета Международной конференции по компьютерному контролю (CAV). [16]
Ссылки [ править ]
- ^ «Кен Макмиллан | Департамент компьютерных наук» . Компьютерные науки, Техасский университет в Остине: преподаватели и исследователи .
- ^ «Кеннет Макмиллан - Проект математической генеалогии» . Проект «Математическая генеалогия» . Американское математическое общество (AMS) . Проверено 21 июня 2023 г.
- ^ «Кеннет Макмиллан — награда ACM» . Награды.acm.org . Ассоциация вычислительной техники . Проверено 21 июня 2023 г.
- ^ «Кеннет Л. Макмиллан — награда ACM» . Награды.acm.org . Ассоциация вычислительной техники (ACM) — Премия Пэрис Канеллакис . Проверено 21 июня 2023 г.
- ^ «WayBackMachine — Кеннет Макмиллан из Microsoft Research» . Майкрософт . Архивировано из оригинала 26 марта 2019 г. Проверено 26 марта 2019 г.
- ^ Твиттер https://twitter.com/UTCompSci/status/1365040812359176193?lang=en . Проверено 21 июня 2023 г.
{{cite web}}
: Отсутствует или пусто|title=
( помощь ) - ^ «Бесплатная загрузка средства проверки моделей SMV» . Скачать бесплатно программу проверки моделей SMV . Проверено 21 июня 2023 г.
- ^ Макмиллан, КЛ (2006). «Ленивая абстракция с интерполянтами» . Компьютерная проверка . Конспекты лекций по информатике. Том. 4144. стр. 123–136. дои : 10.1007/11817963_14 . ISBN 978-3-540-37406-0 .
{{cite book}}
:|journal=
игнорируется ( помогите ) - ^ Бьорнер, Николай; Гурфинкель, Арье; Макмиллан, Кен; Рыбальченко, Андрей (2015). «Решатели предложений Horn для проверки программ» . Решатели предложений Horn для проверки программного обеспечения . Конспекты лекций по информатике. Том. II. стр. 24–51. дои : 10.1007/978-3-319-23534-9_2 . ISBN 978-3-319-23534-9 .
{{cite book}}
:|journal=
игнорируется ( помогите ) - ^ Падон, Одед; Макмиллан, Кеннет; Ауроджит, Панда; Мули, Сагив; Шарон, Шохам (2016). «Плющ: Проверка безопасности путем интерактивного обобщения» . Уведомления ACM SIGPLAN . 51 (6): 614–630. дои : 10.1145/2980983.2908118 .
- ^ «Самая влиятельная награда POPL Paper» . СИГПЛАН АСМ.
- ^ «ЛИКС-Архив» .
- ^ «Премия Аллена Ньюэлла CMU за выдающиеся достижения в области исследований — прошлые победители» . Университет Карнеги-Меллон . Проверено 21 июня 2023 г.
- ^ «Премия КАВ» . Международная конференция по компьютерной верификации.
- ^ «Награда за техническое совершенство – SRC» . Корпорация исследований полупроводников . Проверено 21 июня 2023 г.
- ^ «Международная конференция по компьютерной верификации» . i-cav.org . Проверено 21 июня 2023 г.