Edmund M. Clarke
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 modifica
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 modifica
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 modifica
Enllaços externs modifica
| A Wikimedia Commons hi ha contingut multimèdia relatiu a: Edmund M. Clarke |
- 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