Ernest Allen Emerson II (nacido el 2 de junio de 1954), más conocido como E. Allen Emerson, es un informático estadounidense y ganador del Premio Turing 2007 . Es profesor y catedrático emérito de Regents en la Universidad de Texas en Austin , Estados Unidos.
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 la lógica modal incluyen la introducción de la lógica de árbol de cálculo (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 . Sus primeras experiencias con la informática incluyeron exposición a BASIC , Fortran y ALGOL 60 en el Dartmouth Time Sharing System y las computadoras de grandes sistemas Burroughs . [1] Luego recibió una Licenciatura 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 la década de 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 este 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 en una tecnología de verificación altamente efectiva que se adopta ampliamente 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 para verificar formalmente diseños de sistemas, que se usa ampliamente en la industria del hardware informático y está comenzando a mostrarse muy prometedor también en la verificación de software y otras áreas.
{{cite book}}: |journal=ignorado ( ayuda )[…] fue autor de artículos fundamentales que fundaron lo que se ha convertido en el campo de gran éxito de la verificación de modelos.