Edmund M. Clarke
![]() Edmund Clarke, el 2006 ![]() | |
Biografia | |
---|---|
Naixement | 27 juliol 1945 ![]() Newport News (Virgínia) ![]() |
Mort | 22 desembre 2020 ![]() Pittsburgh (Pennsilvània) ![]() |
Causa de mort | COVID-19 ![]() |
Nacionalitat | Estats Units |
Formació | Universitat de Virgínia Universitat Duke Universitat Cornell |
Tesi acadèmica | Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems (1976) |
Es coneix per | Verificació de models |
Activitat | |
Camp de treball | Ciència computacional i ciències de la computació ![]() |
Ocupació | Informàtica |
Organització | Universitat Duke Harvard University Universitat Carnegie Mellon |
Membre de | Acadèmia Americana de les Arts i les Ciències (2011–) Acadèmia Nacional d'Enginyeria (2005–) Association for Computing Machinery (membre de l'Association for Computing Machinery) (1998–) Institut d'Enginyers Elèctrics i Electrònics ![]() |
Alumnes | E. Allen Emerson ![]() |
Obra | |
Estudiant doctoral | Bud Mishra, E. Allen Emerson, Sicun Gao (en) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Premis Premi Turing (2007) | |
Lloc web | cs.cmu.edu… ![]() |
Edmund Melson Clarke, Jr. (Newport News, 27 de juliol de 1945 – 22 de desembre de 2020) fou un informàtic i acadèmic notable per haver desenvolupat la verificació de models, un mètode per a verificar formalment dissenys de maquinari i programari. Ocupà la càtedra FORE Systems d'Informàtica a la Universitat Carnegie Mellon. Clarke, juntament amb E. Allen Emerson i Joseph Sifakis, va rebre el Premi Turing de 2007, atorgat per l'ACM.
Biografia
Clarke es va llicenciar en matemàtiques a la Universitat de Virgínia, a Charlottesville, el 1967; va obtenir un màster també en matemàtiques a la Universitat Duke de Durham, el 1968, i el doctorat en Informàtica a la Universitat Cornell, d'Ithaca el 1976.[1] Després de doctorar-se, va fer de professor al departament d'informàtica de Duke durant dos anys. El 1978 va canviar a la Harvard University, a Cambridge, Massachusetts, on fou professor ajudant d'Informàtica. Va marxar de Harvard el 1982 per anar al departament d'Informàtica de la Universitat Carnegie Mellon, de Pittsburgh, Pennsilvània. Fou nomenat professor titular el 1989. El 1995 va obtenir la primera càtedra patrocinada per FORE Systems de Carnegie Mellon.[2]
Feina
La seva recerca es va concentrar en la verificació de programari i maquinari i en la demostració automàtica de teoremes. En la seva tesi doctoral, va demostrar que algunes estructures de control dels llenguatges de programació no tenien sistemes de demostració bons en lògica de Hoare. El 1981, ell i el seu estudiant de doctorat E. Allen Emerson van proposar per primera vegada l'ús de la verificació de models com a tècnica per als sistemes concurrents d'autòmats finits. El seu grup va ser pioner en l'ús de verificació de models per a verificació de maquinari i també va desenvolupar la verificació simbòlica utilitzant diagrames de decisió binària. A més, el seu grup de recerca va desenvolupar el primer demostrador de teoremes paral·lel (Parthenon) i el primer basat en un sistema de computació simbòlic (Analytica).[2] El 2009, va liderar la creació del centre CMACS (Computational Modeling and Analysis of Complex Systems, modelització computacional i anàlisi de sistemes complexos), patrocinat per la National Science Foundation. Aquest centre té un equip d'investigadors repartits en múltiples universitats, que apliquen interpretació abstracta i verificació de models a sistemes biològics i incrustats.
Referències
Enllaços externs
![](http://upload.wikimedia.org/wikipedia/commons/thumb/4/4a/Commons-logo.svg/30px-Commons-logo.svg.png)
- Edmund M. Clarke al Mathematics Genealogy Project.
- Pàgina personal a Carnegie Mellon University
- Anunci del premi Turing
- Llibre de Verificació de Models
- Pàgina del CMACS
- Llista de publicacions Arxivat 2016-02-20 a Wayback Machine. a Microsoft Academic Search