Ernest Allen Emerson II (2 de junio de 1954 - 15 de octubre de 2024) fue un científico informático estadounidense y ganador del premio Turing en 2007. Fue profesor y presidente de la junta de regentes de la Universidad de Texas en Austin .
Emerson es reconocido junto con Edmund M. Clarke y Joseph Sifakis por la invención y desarrollo de la verificación de modelos , una técnica utilizada en la verificación formal de software y hardware. [1] Sus contribuciones a la lógica temporal y lógica modal incluyen la introducción de la lógica de árbol de cómputo (CTL) [2] y su extensión CTL* , [3] que se utilizan en la verificación de sistemas concurrentes . También es reconocido junto con otros por desarrollar la verificación de modelos simbólicos para abordar la explosión combinatoria que surge en muchos algoritmos de verificación de modelos. [4]
Emerson nació en Dallas, Texas , el 2 de junio de 1954. Sus primeras experiencias con la informática incluyeron exposición a BASIC , Fortran y ALGOL 60 en el Dartmouth Time Sharing System y en las computadoras de sistemas grandes de Burroughs . [1] Recibió una licenciatura en Ciencias en matemáticas de la Universidad de Texas en Austin en 1976 y un doctorado en Filosofía en matemáticas aplicadas en la Universidad de Harvard en 1981. [1]
A principios de los años 1980, Emerson y su asesor de doctorado, Edmund M. Clarke, desarrollaron técnicas para verificar un sistema de estados finitos frente a una especificación formal . Acuñaron el término "verificación de modelos" para el concepto, que fue estudiado de forma independiente por Joseph Sifakis en Europa. [1] Este sentido de la palabra modelo coincide con el uso de la teoría de modelos en lógica matemática : el sistema se denomina modelo de la especificación.
El trabajo de Emerson sobre verificación de modelos incluyó lógicas temporales tempranas e influyentes para describir especificaciones y técnicas para reducir la explosión del espacio de estados. [1]
En 2007, Emerson, Clarke y Sifakis ganaron el premio Turing. [1] La cita dice:
por su papel en el desarrollo de Model-Checking como una tecnología de verificación altamente efectiva que es ampliamente adoptada en las industrias de hardware y software.
Además del premio Turing, Emerson recibió el premio ACM Paris Kanellakis de 1998 , junto con Randal Bryant , Clarke y Kenneth L. McMillan por el desarrollo de la verificación de modelos simbólicos. [4] La cita dice:
Por su invención de la verificación de modelos simbólicos, un método de verificación formal de diseños de sistemas, que se utiliza ampliamente en la industria del hardware de computadoras y que está empezando a mostrar resultados muy prometedores también en la verificación de software y otras áreas.
Emerson murió en su casa de Austin el 15 de octubre de 2024, a la edad de 70 años. [5] [6]
[…] fue autor de artículos fundamentales que fundaron lo que se ha convertido en el campo altamente exitoso de la verificación de modelos.