Ernest Allen Emerson (Dallas, 2 de junho de 1954 – 15 de outubro de 2024) foi um informático estadunidense. Juntamente com Edmund Clarke realizou trabalho pioneiro na área de verificação de modelos.ACM Turing Award Honors Founders of Automatic Verification Technology That Enables Faster, More Reliable Designs, University of Texas at Austin, 4 de fevereiro de 2008
Emerson é reconhecido junto com Edmund M. Clarke e Joseph Sifakis pela invenção e Desenvolvimento de Model Checking, técnica utilizada na verificação formal de software e hardware. Suas contribuições para a lógica temporal e a lógica modal incluem a introdução da lógica da árvore computacional (CTL) e sua extensão CTL*, que são usadas na verificação de sistemas concorrentes. Ele também é reconhecido, juntamente com outros, por desenvolver a verificação de modelos simbólicos para lidar com a explosão combinatória que surge em muitos algoritmos de verificação de modelos."PRÊMIOS - E. ALLEN EMERSON - 'Prêmio ACM AM Turing' e 'Prêmio Paris Kanellakis de Teoria e Prática'"
Carreira No início da década de 1980, Emerson e seu orientador de doutorado, Edmund M. Clarke, desenvolveram técnicas para verificar um sistema de estados finitos em relação a uma especificação formal. Eles cunharam o termo verificação de modelo para o conceito, que foi estudado independentemente por Joseph Sifakis na Europa. Este sentido da palavra modelo corresponde ao uso da teoria dos modelos na lógica matemática: o sistema é chamado de modelo da especificação.
O trabalho de Emerson na verificação de modelos incluiu lógicas temporais antigas e influentes para descrever especificações e técnicas para reduzir a explosão do espaço de estados.
Morte Emerson morreu em sua casa em Austin em 15 de outubro de 2024, aos 70 anos.
Ligações externas
Categoria:Prêmio Turing Categoria:Professores da Universidade do Texas em Austin Categoria:Cientistas da computação dos Estados Unidos Categoria:Alunos da Universidade Harvard Categoria:Alunos da Universidade do Texas em Austin