Edmund Melson Clarke, Jr. (27 de julio de 1945-22 de diciembre de 2020) fue un científico informático y académico estadounidense conocido por desarrollar la verificación de modelos , un método para verificar formalmente diseños de hardware y software . Fue profesor de Ciencias de la Computación FORE Systems en la Universidad Carnegie Mellon . Clarke, junto con E. Allen Emerson y Joseph Sifakis , recibieron el premio ACM Turing 2007 .
Nacido en Newport News, Virginia , Clarke recibió una licenciatura en matemáticas de la Universidad de Virginia , Charlottesville , en 1967, una maestría en matemáticas de la Universidad de Duke , Durham Carolina del Norte , en 1968, y un doctorado. Licenciado en Ciencias de la Computación por la Universidad de Cornell , Ithaca, Nueva York, 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 Ciencias de la Computación 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 beneficiario de la Cátedra FORE Systems , una cátedra subvencionada en la Escuela de Ciencias de la Computación Carnegie Mellon . Se convirtió en profesor universitario en 2008 y profesor emérito en 2015. [2]
Murió de COVID-19 en diciembre de 2020, a los 75 años, durante la pandemia de COVID-19 en Pensilvania . [3] [4]
Los intereses de Clarke incluían la verificación de software y hardware y la demostración automática de teoremas . En su doctorado. En su tesis demostró que ciertas estructuras de control de lenguajes de programación no tenían buenos sistemas de prueba 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 doctorado de Kenneth McMillan. tesis, que recibió el Premio de Tesis Doctoral ACM . Además, su grupo de investigación desarrolló el primer demostrador de teoremas de resolución paralela (Parthenon) y un demostrador de teoremas basado en un sistema de cálculo simbólico (Analytica) [5] . En 2009, lideró la creación del centro de Análisis y Modelado Computacional de Sistemas Complejos (CMACS), financiado por la Fundación Nacional de Ciencias . Este centro cuenta con un equipo de investigadores, que abarca varias universidades, que aplican interpretación abstracta y verificación de modelos a sistemas biológicos e integrados .
Clarke era miembro de la ACM y del IEEE . Recibió un Premio a la Excelencia Técnica de Semiconductor Research Corporation en 1995 y un Premio Allen Newell a la Excelencia en Investigación del Departamento de Ciencias de la Computación de Carnegie Mellon en 1999. Fue coganador junto con Randal Bryant , E. Allen Emerson y Kenneth. McMillan del premio ACM Paris Kanellakis en 1999 por el desarrollo de la verificación de modelos simbólicos . En 2004 recibió el premio Harry H. Goode Memorial de la IEEE Computer Society por sus 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 el 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". En 2012, recibió un doctorado honorario de la Universidad Técnica de Viena por sus destacadas contribuciones al campo de la informática. Recibió el Premio Bower y el Premio por Logros en Ciencias del Instituto Franklin en 2014 por "su papel de liderazgo en la concepción y desarrollo de técnicas para verificar automáticamente la exactitud 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 .
