Edmund M. Clarke

Edmund M. Clarke Immagine in Infobox. Edmund M. Clarke nel 2006. Biografia
Nascita 27 luglio 1945
Newport News
Morte 22 dicembre 2020(all'età di 75 anni)
Pittsburgh
Nome nella lingua madre Edmund Melson Clarke, Jr.
Nazionalità Americano
Formazione Università della Virginia (1967)
Duke University (1968)
Cornell University (1976)
Attività Informatico , professore universitario , ricercatore , ingegnere , matematico
Altre informazioni
Lavorato per Carnegie-Mellon University , Duke University (1976) , Università di Harvard (1978) , Cornell University (1982)
le zone Scienza dell'informazione ( in ) , computer
Membro di Institute of Electrical and Electronics Engineers
Association for Computing Machinery
Accademia nazionale di ingegneria degli Stati Uniti (2005)
Accademia americana delle arti e delle scienze (2011)
Supervisore Robert Lee Constable
Sito web (en)  www.cs.cmu.edu/~emc
Premi Premio Turing (2007)

Edmund Melson Clarke, Jr. (27 luglio 1945 - 22 dicembre 2020) è uno scienziato informatico accademico noto per i suoi contributi al controllo dei modelli , un metodo di verifica dei progetti software e hardware. È titolare della cattedra FORE Systems  (in) in IT presso la Carnegie-Mellon University . Clarke è stato uno dei tre destinatari, insieme a E. Allen Emerson e Joseph Sifakis , del Premio Turing 2007, assegnato dall'Association for Computing Machinery (ACM).

Biografia

Clarke ha conseguito una laurea in matematica presso l' Università della Virginia a Charlottesville nel 1967, quindi un master in matematica presso la Duke University di Durham (North Carolina) nel 1968 e un dottorato di ricerca in informatica presso la Cornell University , a Ithaca (New York) nel 1976. Dopo il dottorato, ha insegnato per due anni al dipartimento di informatica della Duke University e nel 1978 è partito per la Harvard University di Cambridge (Massachusetts) dove è assistente professore di informatica nel dipartimento di ingegneria e scienze applicate. Dopo Harvard, nel 1982 è entrato a far parte del dipartimento di informatica della Carnegie-Mellon University di Pittsburgh . È diventato professore ordinario nel 1989. Nel 1995, è diventato il primo titolare della cattedra FORE Systems  (in) una cattedra collegata alla Carnegie Mellon School of Computer Science  (in) .

È membro della Sigma Xi Scientific Society e della Phi Beta Kappa Alumni Association .

Opera

Gli interessi scientifici di Clarke includono la verifica e la convalida di software e hardware per computer e la dimostrazione automatica dei teoremi .

Nella sua tesi di dottorato, mostra che alcune strutture di controllo dei linguaggi di programmazione non hanno buoni sistemi di prova nella logica di Hoare . Nel 1981, lui e il suo dottorando Allen Emerson furono i primi a proporre l'uso del controllo dei modelli come tecnica di verifica per sistemi concorrenti con un numero finito di stati.

Il suo gruppo di ricerca è stato allora un pioniere nell'uso del model check per il controllo delle apparecchiature . Il modello di controllo simbolico, utilizzando i diagrammi decisionali binari (o BDD) è sviluppato anche dal suo gruppo. La tesi di dottorato di Kenneth McMillan sviluppa un'importante tecnica di questo tema; ha ricevuto la tesi Excellence Award dalla ACM .

Inoltre, il gruppo di ricerca di Clarke ha sviluppato il primo dimostratore di teoremi paralleli ( Partenone ) e il primo dimostratore di teoremi basato su un sistema di calcolo simbolico ( Analytica ).

Nel 2009 ha guidato la creazione del centro CMACS (Computational Modeling and Analysis of Complex Systems), finanziato dalla National Science Foundation . Questo centro comprende un gruppo di ricercatori, distribuiti in diverse università, che applicano l'interpretazione astratta e il controllo dei modelli a sistemi biologici e sistemi incorporati.

Lavoro

Premi e riconoscimenti

Riferimenti

  1. Elenco dei destinatari sul sito Carnegie-Mellon .
  2. Annuncio sul sito web di ACM .
  3. annuncio sul sito web IEEE .

link esterno