stringtranslate.com

Kenneth McMillan

Ken McMillan (centro) con David L. Dill (abajo a la izquierda), Robert P. Kurshan (arriba a la izquierda) y Edmund Clarke (derecha) en FLoC 2006.

Kenneth L. McMillan es un científico informático estadounidense que trabaja en el área de métodos formales , lógica y lenguajes de programación . Es profesor en el departamento de informática de la Universidad de Texas en Austin , donde ocupa la Cátedra Centenario Admiral BR Inman en Teoría de la Computación. [1]

Carrera

McMillan recibió su doctorado. desde Universidad Carnegie Mellon en 1992, bajo la dirección de Edmund M. Clarke . [2] Se le atribuye haber inventado la verificación de modelos simbólicos durante su trabajo de tesis, que le valió el Premio de Tesis Doctoral ACM de 1992 , el premio de tesis doctoral más alto otorgado por la Asociación de Maquinaria de Computación (ACM). [3] También ganó el Premio ACM Paris Kanellakis de Teoría y Práctica de 1998 junto con Randal Bryant , Edmund Clarke y E. Allen Emerson por su trabajo en la verificación de modelos simbólicos. [4] McMillan trabajó posteriormente en Bell Labs , Cadence Berkeley Labs y fue investigador principal en Microsoft Research, Redmond [5] antes de unirse a la facultad de la Universidad de Texas en Austin en 2021. [6]

Investigación

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

Servicio

McMillan actualmente forma parte del comité directivo de la Conferencia Internacional sobre Verificación Asistida por Computadora (CAV). [dieciséis]

Referencias

  1. ^ "Ken McMillan | Departamento de Ciencias de la Computación". Ciencias de la Computación, Universidad de Texas en Austin: profesores e investigadores .
  2. ^ "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 .
  3. ^ "Kenneth McMillan - Premios ACM". premios.acm.org . Asociación para Maquinaria de Computación . Consultado el 21 de junio de 2023 .
  4. ^ "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 .
  5. ^ "WayBackMachine - Kenneth McMillan en Microsoft Research". Microsoft . Archivado desde el original el 26 de marzo de 2019 . Consultado el 26 de marzo de 2019 .
  6. ^ 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 )
  7. ^ "Descarga gratuita del Comprobador de modelos SMV". Descarga gratuita del Comprobador de modelos SMV . Consultado el 21 de junio de 2023 .
  8. ^ 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. ISBN 978-3-540-37406-0. {{cite book}}: |journal=ignorado ( ayuda )
  9. ^ 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. ISBN 978-3-319-23534-9. {{cite book}}: |journal=ignorado ( ayuda )
  10. ^ 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.
  11. ^ "Premio al artículo POPL más influyente". SIGPLAN ACM.
  12. ^ "LICS - Archivo".
  13. ^ "Premio CMU Allen Newell a la excelencia en investigación: ganadores anteriores". Universidad de Carnegie mellon . Consultado el 21 de junio de 2023 .
  14. ^ "Premio CAV". Congreso Internacional sobre Verificación Asistida por Computadora.
  15. ^ "Premio a la Excelencia Técnica - SRC". Corporación de Investigación de Semiconductores . Consultado el 21 de junio de 2023 .
  16. ^ "Conferencia Internacional sobre Verificación Asistida por Computadora". i-cav.org . Consultado el 21 de junio de 2023 .