McMillan fue pionero en varias áreas de investigación influyentes en métodos formales. Su trabajo inicial sobre verificación de modelos simbólicos basados en diagramas de decisión binaria culminó con la creación de la familia de verificadores de modelos SMV/nuSMV . [7] También fue pionero en técnicas basadas en la interpolación de Craig en la verificación de modelos de sistemas de estados infinitos. [8] También es conocido por su trabajo en la resolución de la cláusula de cuerno restringida (CHC) [9] y la herramienta de verificación de sistemas distribuidos IVy. [10]
Premios
2014 - Premio POPL al artículo más influyente [11]
^ "Ken McMillan | Departamento de Ciencias de la Computación". Ciencias de la Computación, Universidad de Texas en Austin: profesores e investigadores .
^ "Kenneth McMillan - El proyecto de genealogía de las matemáticas". El Proyecto de Genealogía de las Matemáticas . Sociedad Estadounidense de Matemáticas (AMS) . Consultado el 21 de junio de 2023 .
^ "Kenneth McMillan - Premios ACM". premios.acm.org . Asociación para Maquinaria de Computación . Consultado el 21 de junio de 2023 .
^ "Kenneth L. McMillan - Premios ACM". premios.acm.org . Asociación de Maquinaria de Computación (ACM) - Premio Paris Kanellakis . Consultado el 21 de junio de 2023 .
^ "WayBackMachine - Kenneth McMillan en Microsoft Research". Microsoft . Archivado desde el original el 26 de marzo de 2019 . Consultado el 26 de marzo de 2019 .
^ Gorjeo https://twitter.com/UTCompSci/status/1365040812359176193?lang=en . Consultado el 21 de junio de 2023 .{{cite web}}: Falta o está vacío |title=( ayuda )
^ "Descarga gratuita del Comprobador de modelos SMV". Descarga gratuita del Comprobador de modelos SMV . Consultado el 21 de junio de 2023 .
^ McMillan, KL (2006). "Abstracción perezosa con interpolantes". Verificación asistida por computadora . Apuntes de conferencias sobre informática. vol. 4144, págs. 123-136. doi :10.1007/11817963_14. ISBN978-3-540-37406-0. {{cite book}}: |journal=ignorado ( ayuda )
^ Björner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey (2015). "Solucionadores de cláusulas de bocina para verificación de programas". "Solucionadores de cláusulas de bocina para verificación de software" . Apuntes de conferencias sobre informática. vol. II. págs. 24–51. doi :10.1007/978-3-319-23534-9_2. ISBN978-3-319-23534-9. {{cite book}}: |journal=ignorado ( ayuda )
^ Padón, Oded; McMillan, Kenneth; Aurojit, Panda; Mooly, Sagiv; Sharon, Shoham (2016). "Ivy: verificación de seguridad mediante generalización interactiva". Avisos ACM SIGPLAN . 51 (6): 614–630. doi :10.1145/2980983.2908118.
^ "Premio al artículo POPL más influyente". SIGPLAN ACM.
^ "LICS - Archivo".
^ "Premio CMU Allen Newell a la excelencia en investigación: ganadores anteriores". Universidad de Carnegie mellon . Consultado el 21 de junio de 2023 .
^ "Premio CAV". Congreso Internacional sobre Verificación Asistida por Computadora.
^ "Premio a la Excelencia Técnica - SRC". Corporación de Investigación de Semiconductores . Consultado el 21 de junio de 2023 .
^ "Conferencia Internacional sobre Verificación Asistida por Computadora". i-cav.org . Consultado el 21 de junio de 2023 .