stringtranslate.com

Kenneth L. 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 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 Centenaria Admiral BR Inman en Teoría de la Computación. [1]

Carrera

McMillan recibió su doctorado en la 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 Computacional (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] Posteriormente, McMillan trabajó 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 en la verificación de modelos simbólicos basados ​​en diagramas de decisión binarios culminó en 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 Horn 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). [16]

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 matemática". El proyecto de genealogía matemática . Sociedad Matemática Estadounidense (AMS) . Consultado el 21 de junio de 2023 .
  3. ^ "Kenneth McMillan - Premios ACM". awards.acm.org . Association for Computing Machinery . Consultado el 21 de junio de 2023 .
  4. ^ "Kenneth L. McMillan - Premios ACM". awards.acm.org . Association for Computing Machinery (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. ^ Twitter 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 de SMV Model Checker". Descarga gratuita de SMV Model Checker . Consultado el 21 de junio de 2023 .
  8. ^ McMillan, KL (2006). "Abstracción perezosa con interpoladores". Verificación asistida por computadora . Apuntes de clase en 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. ^ Bjorner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey (2015). "Solucionadores de cláusulas Horn para verificación de programas". Solucionadores de cláusulas Horn para verificación de software . Apuntes de clase en 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. ^ Padon, Oded; McMillan, Kenneth; Aurojit, Panda; Mooly, Sagiv; Sharon, Shoham (2016). "Ivy: Verificación de seguridad mediante generalización interactiva". Avisos SIGPLAN de la ACM . 51 (6): 614–630. doi :10.1145/2980983.2908118.
  11. ^ "Premio al artículo más influyente de POPL". ACM SIGPLAN.
  12. ^ "LICS - Archivo".
  13. ^ "Premio Allen Newell de la CMU a la excelencia en investigación: ganadores anteriores". Universidad Carnegie Mellon . Consultado el 21 de junio de 2023 .
  14. ^ "Premio CAV". Conferencia Internacional sobre Verificación Asistida por Computadora.
  15. ^ "Premio a la Excelencia Técnica - SRC". Semiconductor Research Corporation . 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 .