Ernest Allen Emerson
| ||||||||||||||
Ernest Allen Emerson. Es un científico de la computación y profesor en la Universidad de Texas, Austin, Estados Unidos. Él ganó el 2007 el Premio Turing, junto con Edmund M. Clarke y Joseph Sifakis por su trabajo pionero sobre El Chequeo Modelo (Model Checking en inglés). Ganó en 1998 el premio ACM Paris Kanellakis por Teoría y Práctica para la Comprobación de Modelo Simbólico.
Sumario
Síntesis biográfica
Nació el 2 de junio de 1954 en Dallas, Texas, Estados Unidos.
Estudios realizados
Se interesó en temas científicos y matemáticos. Aprendió cálculo varios años antes de que él comenzara en la escuela pública. Emerson tomó un curso sobre programación de computadoras en la escuela secundaria y se adentró para el Sistema de Intercambio de GE Mark I. Posteriormente, él aprendió lenguaje de programación Fortran y Algol, y corrió programas en una computadora Burroughs B5500.
Emerson estudió en la Universidad de Texas en Austin, donde obtuvo su licenciatura en Matemáticas en 1976. Luego pasó a la escuela de posgrado en la Universidad de Harvard, donde obtuvo un doctorado en Matemáticas Aplicadas (Computer Science) en 1981. Poco después se incorporó a la Universidad de Texas en Austin como un miembro de la facultad y ha permanecido allí desde entonces. Él es ahora Rector de Cátedra y Profesor de Ciencias de la Computación.
Tiene interés en los métodos formales para el establecimiento de la corrección del programa que se remonta a sus días de universidad. Esto fue inspirado en parte por la lectura de un Comunicado de la ACM por parte de Tony Hoare, "Prueba del programa: Encontrar". También fue inspiradora una charla de Zohar Maná en puntos fijos y el Teorema de Tarski-Knaster dado en la década de 1970 en la Universidad de Texas. Él también estaba intrigado por la obra de JW De Bakker, W. P De Roever y Edsger W. Dijkstra.
Emerson es un Investigador "Highly Cited" del Instituto de Ciencias de la Información, un reconocimiento que se da a los 250 investigadores de informática más referenciados. Se ha desempeñado como editor de importantes revistas, incluyendo transacciones de ACM en Lógica Computacional (TOCl), Métodos Formales en Diseño de Sistemas (FMSD), Aspectos Formales de la Informática (FAC), y métodos de la lógica en Ciencias de la Computación (MLC). Es miembro fundador del Comité Directivo de la Conferencia de Métodos Formales Automatizado de Herramientas de Verificación y Análisis (ATVA) y es miembro del comité de dirección de la verificación, comprobación de modelos, e interpretación abstracta. (VMCAI).
Sobre su Comprobación de Modelo Simbólico
Por su invención de la Comprobación de Modelo Simbólico, un método para comprobar formalmente diseños de sistemas, que es ampliamente utilizado en la industria del hardware y está empezando a mostrar una promesa significativa también en la verificación del software y otras áreas. En la década de 1980, inventó la lógica árbol de cómput. Emerson es un miembro de la ACM.
El chequeo de modelo fue inventado en 1981 por Edmund M. Clarke y Emerson. Esta técnica ha permitido comprobar algorítmicamente propiedades lógicas, expresado en una notación llamada lógica temporal, de los sistemas de estados finitos. Clarke y Emerson fueron capaces de utilizar el modelo de chequeos para encontrar algunos errores de diseño muy sutiles de hardware. En 1985, Bryant desarrolló una nueva representación de funciones booleanas, llamado OBDDs (siglas en inglés)(Diagrama Ordenado De Disposición Binaria). La contribución crucial de Bryant era mostrar que mediante la fijación del orden de las pruebas de las variables booleanas en diagramas de decisión binarios, estos diagramas se convierten computacionalmente en muy manejables. McMillan se dio cuenta de que OBDDs puede representar simbólicamente conjuntos de estados en los sistemas del estado de transición. En 1987, se desarrolló una herramienta de software llamada SMV (Verificador de Modelo SImbólico) con la que los sistemas con más de 10 ^ 20 estados podrían ser verificados, y nació la Comprobación de Modelo Simbólico.
Honores y premios
- ACM Premio Paris Kanellakis de Teoría y Práctica, (1998);
- CMU Premio Allen Newell a la Excelencia Investigadora, (1999);
- IEEE Premio Lógica en Ciencias de la Computación de Test-of-Time Award (2006);
- ACM AM Premio Turing (2007).
