Ernest Allen Emerson
| Ernest Allen Emerson | |
|---|---|
.jpg) | |
| Nascimento | 2 de junho de 1954 Dallas, Estados Unidos |
| Morte | 15 de outubro de 2024 (70 anos) Austin |
| Nacionalidade | estadunidense |
| Cidadania | Estados Unidos |
| Alma mater | Universidade Harvard |
| Ocupação | cientista de computação, engenheiro, professor universitário |
| Distinções | Prêmio Paris Kanellakis (1998), Prêmio Turing (2007) |
| Empregador(a) | Universidade do Texas em Austin |
| Orientador(a)(es/s) | Edmund Clarke |
| Campo(s) | ciência da computação |
| Tese | 1981: Branching Time Temporal Logic and the Design of Correct Concurrent Programs |
| Página oficial | |
| http://www.cs.utexas.edu/~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]
Carreira
[editar | editar código-fonte]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.[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]
Morte
[editar | editar código-fonte]Emerson morreu em sua casa em Austin em 15 de outubro de 2024, aos 70 anos.[7]
Referências
- ↑ «We bid farewell to E. Allen Emerson». Heidelberg Laureate Foundation (em inglês). Consultado em 20 de outubro de 2024
- ↑ 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
- ↑ Clarke, Edmund M.; Emerson, E. Allen (1982). Kozen, Dexter, ed. «Design and synthesis of synchronization skeletons using branching time temporal logic». Berlin, Heidelberg: Springer (em inglês): 52–71. ISBN 978-3-540-39047-3. doi:10.1007/BFb0025774. Consultado em 28 de outubro de 2024
- ↑ Emerson, E. Allen; Halpern, Joseph Y. (2 de janeiro de 1986). «"Sometimes" and "not never" revisited: on branching versus linear time temporal logic». J. ACM (1): 151–178. ISSN 0004-5411. doi:10.1145/4904.4999. Consultado em 28 de outubro de 2024
- ↑ "PRÊMIOS - E. ALLEN EMERSON - 'Prêmio ACM AM Turing' e 'Prêmio Paris Kanellakis de Teoria e Prática'"
- ↑ a b «E. Allen Emerson - A.M. Turing Award Laureate». amturing.acm.org. Consultado em 28 de outubro de 2024
- ↑ «We bid farewell to E. Allen Emerson». Heidelberg Laureate Foundation (em inglês). Consultado em 28 de outubro de 2024
Ligações externas
[editar | editar código-fonte]- Ernest Allen Emerson (em inglês) no Mathematics Genealogy Project
- «Página pessoal no sítio da Universidade do Texas em Austin» (em inglês)
| Precedido por Frances Allen |
Prêmio Turing 2007 com Edmund Clarke e Joseph Sifakis |
Sucedido por Barbara Liskov |
