Edmund M. Clarke

De Viquipèdia
Salta a: navegació, cerca
Infotaula de personaEdmund Melson Clarke, Jr.
Edmund Clarke FLoC 2006.jpg
Edmund Clarke, el 2006
Dades biogràfiques
Naixement 27 de juliol de 1945 (1945-07-27) (72 anys)
Newport News
Nacionalitat Estats Units
Alma mater Universitat de Virgínia
Universitat Duke
Universitat Cornell
Tesi Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems (1976)
Es coneix per Verificació de models
Activitat professional
Camp de treball Ciència computacional
Ocupació Informàtica
Organització Universitat Duke
Harvard University
Universitat Carnegie Mellon
Premis i reconeixements
Premi Turing (2007)

Lloc web Lloc web oficial
Modifica dades a Wikidata

Edmund Melson Clarke, Jr. (nascut el 27 de juliol de 1945) és 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. Ocupa 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 | modifica el codi]

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 | modifica el codi]

La seva recerca s'ha concentrat 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 | modifica el codi]

Enllaços externs[modifica | modifica el codi]

A Wikimedia Commons hi ha contingut multimèdia relatiu a: Edmund M. Clarke Modifica l'enllaç a Wikidata