Edmund M. Clarke

Edmund Melson Clarke, Jr.

(2006)
Biografia
Naixement	27 juliol 1945 Newport News (Virgínia)
Mort	22 desembre 2020 (75 anys) 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) , David L. Dill (en) , Kenneth L. McMillan, Marius Minea (en) , Sergio Vale Aguiar Campos (en) , Somesh Jha (en) , Xudong Zhao (en) , David Elsey Long (en) , Jerry Robert Burch (en) , Michael Browne (en) , Wilfredo Rogelio Marrero (en) , Aravinda Prasad Sistla (en) i Alex David Groce (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. 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.

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). 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.

Enllaços externs

• Edmund M. Clarke al Mathematics Genealogy Project.
• Pàgina personal a Carnegie Mellon University
• Llibre de Verificació de Models
• Pàgina del CMACS