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