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 los diseños de hardware y software . Fue profesor de informática de FORE Systems en la Universidad Carnegie Mellon . Clarke, junto con E. Allen Emerson y Joseph Sifakis , recibió el premio ACM Turing en 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 NC , en 1968, y un doctorado 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 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 destinatario de la Cátedra de Sistemas FORE , una cátedra dotada en la Escuela de Ciencias de la Computación Carnegie Mellon . Se convirtió en profesor universitario en 2008 y se convirtió en profesor emérito en 2015. [2]
Murió por 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 tesis doctoral demostró que ciertas estructuras de control de lenguaje de programación no tenían buenos sistemas de prueba de estilo Hoare . En 1981, él y su estudiante de doctorado E. Allen Emerson propusieron 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 simbólica de modelos mediante diagramas de decisión binarios . Esta importante técnica fue el tema de la tesis doctoral de Kenneth McMillan, que recibió un premio de disertación 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 computación simbólica (Analytica) [5] . 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 varias universidades, que aplican interpretación abstracta y verificación de modelos a sistemas biológicos e integrados .
Clarke fue miembro de la 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 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 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 las Artes y las 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 TU Wien por sus destacadas contribuciones al campo de la informática. Recibió el Premio Bower 2014 y el Premio al Logro en Ciencia del Instituto Franklin por "su papel líder 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 la medicina". Fue miembro de Sigma Xi y Phi Beta Kappa .
