|
Ernest Allen Emerson
Ernest Allen Emerson (Dallas, 2 de junho de 1954 – 15 de outubro de 2024)[1] foi um informático estadunidense. Juntamente com Edmund Clarke realizou trabalho pioneiro na área de verificação de modelos.[2] 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)[3] e sua extensão CTL*,[4] 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.[5] CarreiraNo 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.[6] 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.[6] MorteEmerson morreu em sua casa em Austin em 15 de outubro de 2024, aos 70 anos.[7] Referências
Ligações externas
|
|||||||||||||||||||||||||||||||||||
.jpg)
Portal di Ensiklopedia Dunia
