Edmund Melson Clarke, Jr. (27 de julio de 1945-22 de diciembre de 2020) fue un científico informático y académico estadounidense destacado por desarrollar la verificación de modelos , un método para verificar formalmente los diseños de hardware y software. Fue profesor emérito de informática de FORE Systems en la Universidad Carnegie Mellon . Clarke, junto con E. Allen Emerson y Joseph Sifakis , recibió el 2007 Association for Computing Machinery A.M. Premio Turing .
Edmund M. Clarke | |
---|---|
Nació | Edmund Melson Clarke, Jr. 27 de julio de 1945 Newport News, Virginia , Estados Unidos |
Fallecido | 22 de diciembre de 2020 | (75 años)
Nacionalidad | americano |
alma mater | Universidad de Cornell |
Conocido por | Comprobación de modelo |
Premios | Premio AM Turing |
Carrera científica | |
Campos | Ciencias de la Computación |
Instituciones | Universidad de Carnegie mellon |
Tesis | Teoremas de completitud e incompletitud para sistemas axiomáticos similares a Hoare (1976) |
Asesor de doctorado | Robert Lee Constable |
Estudiantes de doctorado | |
Sitio web | www |
Biografía
Clarke recibió un BA grado en matemáticas de la Universidad de Virginia , Charlottesville, VA , en 1967, un MA grado en matemáticas de la Universidad de Duke , Durham NC , en 1968, y un Ph.D. Licenciado en Ciencias de la Computación de la Universidad de Cornell , Ithaca NY en 1976. Después de recibir su doctorado, enseñó en el Departamento de Ciencias de la Computación de la Universidad de Duke durante dos años. En 1978 se trasladó a la Universidad de Harvard , Cambridge, MA, donde fue profesor asistente de informática en la División de Ciencias Aplicadas . Dejó Harvard en 1982 para unirse a la facultad del Departamento de Ciencias de la Computación de la Universidad Carnegie Mellon , Pittsburgh, PA . Fue nombrado profesor titular en 1989. En 1995 se convirtió en el primer destinatario de la cátedra de sistemas FORE , una cátedra en la Carnegie Mellon School of Computer Science . Se convirtió en profesor universitario en 2008 y profesor emérito en 2015. [2] Murió de COVID-19 durante la pandemia de COVID-19 en Pensilvania en 2020. [3] [4]
Trabaja
Los intereses de Clarke incluían la verificación de software y hardware y la demostración automática de teoremas . En su Ph.D. tesis demostró que ciertas estructuras de control del lenguaje de programación no tenían buenos sistemas de prueba al estilo Hoare . En 1981 él y su Ph.D. El estudiante E. Allen Emerson propuso por primera vez el uso de la verificación de modelos como técnica de verificación para sistemas concurrentes de estados finitos . Su grupo de investigación fue pionero en el uso de la verificación de modelos para la verificación de hardware . Su grupo también desarrolló la verificación de modelos simbólicos utilizando diagramas de decisión binarios . Esta importante técnica fue el tema del Ph.D. de Kenneth McMillan. tesis, que recibió un Premio ACM de Disertación de Doctorado . Además, su grupo de investigación desarrolló el primer demostrador de teoremas de resolución paralela (Partenón) y el primer demostrador de teoremas basado en un sistema de cálculo simbólico (Analytica). En 2009, lideró la creación del centro de Modelado y Análisis Computacional de Sistemas Complejos (CMACS), financiado por la National Science Foundation . Este centro cuenta con un equipo de investigadores, que abarca múltiples universidades, aplicando interpretación abstracta y verificación de modelos a sistemas biológicos e integrados.
Reconocimiento profesional
Clarke era miembro del ACM y del IEEE . Recibió un premio a la excelencia técnica de la Semiconductor Research Corporation en 1995 y un premio Allen Newell a la excelencia en la investigación del Departamento de Ciencias de la Computación de Carnegie Mellon en 1999. Fue co-ganador junto con Randal Bryant , E. Allen Emerson y Kenneth McMillan del premio ACM Paris Kanellakis en 1999 por el desarrollo de la comprobación de modelos simbólicos . En 2004 recibió el premio en memoria de IEEE Computer Society Harry H. Goode por contribuciones significativas y pioneras a la verificación formal de sistemas de hardware y software, y por el profundo impacto que estas contribuciones han tenido en la industria electrónica. Fue elegido miembro de la Academia Nacional de Ingeniería en 2005 por sus contribuciones a la verificación formal de la corrección del hardware y software. Fue elegido miembro de la Academia Estadounidense de Artes y Ciencias en 2011. Recibió el premio Herbrand en 2008 en "reconocimiento a su papel en la invención de la verificación de modelos y su liderazgo sostenido en el área durante más de dos décadas". Recibió el Premio Bower 2014 y el Premio al Logro en Ciencias del Instituto Franklin por "su papel principal en la concepción y desarrollo de técnicas para verificar automáticamente la corrección de una amplia gama de sistemas informáticos, incluidos los que se encuentran en el transporte, las comunicaciones y medicamento." Fue miembro de Sigma Xi y Phi Beta Kappa .
Ver también
- Lista de pioneros en informática
Referencias
- ^ Edmund Melson Clarke, Jr.
- ^ "Edmund M. Clarke" . Cs.cmu.edu . Consultado el 24 de diciembre de 2020 .
- ^ James S. Clarke [@Jim_in_Oregon] (22 de diciembre de 2020). "Mi padre, Edmund M Clarke, falleció hoy de Covid. [...]" (Tweet) - vía Twitter .
- ^ "Edmund Clarke fue pionero en métodos para detectar errores de software, hardware | Escuela de Ciencias de la Computación Carnegie Mellon" . Cs.cmu.edu . Consultado el 24 de diciembre de 2020 .
enlaces externos
- Edmund M. Clarke en el Proyecto de genealogía matemática
- Página de inicio de la Universidad Carnegie Mellon
- Biografía en línea desde la página de inicio
- Anuncio del premio Turing
- Libro de cheques modelo
- Página de inicio de CMACS
- Lista de publicaciones de Microsoft Academic