Edmund M. Clarke
Pour les articles homonymes, voir Clarke.
Edmund M. Clarke
Edmund M. Clarke en 2006.
| Naissance |  Newport News |
|---|---|
| Décès | (à 75 ans) Pittsburgh |
| Nom dans la langue maternelle | Edmund Melson Clarke, Jr. |
| Nationalité | américaine |
| Formation | Université de Virginie (baccalauréat universitaire) () Université Duke (maîtrise ès arts) () Université Cornell (doctorat) () |
| Activités | Informaticien, ingénieur, professeur d'université, mathématicien |
| A travaillé pour | |
|---|---|
| Membre de | |
| Directeur de thèse | |
| Site web | (en) www.cs.cmu.edu/~emc |
| Distinctions | Prix Turing () Liste détaillée ACM Fellow () Prix Paris-Kanellakis () Prix commémoratif Harry H. Goode () Prix Turing () Prix Herbrand () Médaille Benjamin-Franklin () Bower Award and Prize for Achievement in Science () Membre de l'Académie américaine des arts et des sciences Membre de l'IEEE Docteur honoris causa de l'université technique de Vienne |
modifier - modifier le code - modifier Wikidata
Edmund Melson Clarke, Jr. ( - ) est un informaticien universitaire connu pour ses contributions au model checking, une méthode de vérification de conceptions de logiciel et matériel. Il est titulaire de la chaire FORE Systems (en) en informatique à l'université Carnegie-Mellon. Clarke a été l'un des trois récipiendaires, avec E. Allen Emerson et Joseph Sifakis, du prix Turing 2007, décerné par l'Association for Computing Machinery (ACM).
Biographie
Clarke obtient un B.A. en mathématiques à l'université de Virginie de Charlottesville en 1967, puis une maîtrise (M.A.) en mathématiques à l'université Duke de Durham (Caroline du Nord) en 1968, et un Ph.D. en informatique à l'université Cornell, à Ithaca (New York) en 1976. Après son Ph.D., il enseigne au département d'informatique de l'université Duke pendant deux ans, et en 1978 il part pour l'université Harvard à Cambridge (Massachusetts) où il est professeur assistant en informatique dans le département d’ingénierie et de sciences appliquées. Après Harvard, il rejoint en 1982 le département d'informatique de l'université Carnegie-Mellon à Pittsburgh. Il devient professeur titulaire en 1989. En 1995, il est le premier titulaire de la chaire FORE Systems (en), une chaire attachée à la Carnegie Mellon School of Computer Science (en).
Il est membre de la société scientifique Sigma Xi et de l'association d'anciens élèves Phi Beta Kappa.
Œuvre
Les intérêts scientifiques de Clarke comprennent la vérification et la validation de logiciels et de matériels informatiques, et la démonstration automatique de théorèmes.
Dans sa thèse de Ph.D., il montre que certaines structures de contrôle de langages de programmation ne possèdent pas de bons systèmes de preuve en logique de Hoare. En 1981, lui et son étudiant en Ph.D. Allen Emerson sont les premiers à proposer l'usage du model checking comme technique de vérification pour des systèmes concurrents à un nombre fini d'états.
Son groupe de recherche est alors pionnier dans l'usage du model checking pour la vérification du matériel. Le model checking symbolique, utilisant les diagrammes de décision binaire (ou BDD) est également développé par son groupe. La thèse de Ph. D. de Kenneth McMillan développe une technique importante de ce thème ; elle a obtenu le prix d'excellence des thèses de l'ACM.
De plus, le groupe de recherche de Clarke a développé le premier démonstrateur de théorèmes parallèle (Parthenon) et le premier démonstrateur de théorèmes basé sur un système de calcul symbolique (Analytica).
En 2009, il dirige la création du centre CMACS (Computational Modeling and Analysis of Complex Systems), financé par la National Science Foundation. Ce centre comprend un groupe de chercheurs, répartis sur plusieurs universités, qui appliquent l'interprétation abstraite et le model checking aux systèmes biologiques et aux systèmes embarqués.
Ouvrage
- (en) Edmund M. Clarke, Orna Grumberg et Doron A. Peled, Model Checking, The MIT Press, , 314 p. (ISBN 978-0-262-03270-4, lire en ligne)
Prix et distinctions
- Clarke est Fellow de l'ACM et de l'IEEE.
- En 1995, il obtient un prix d'excellence technique de l'association Semiconductor Research Corporation (en), et en 1999 le prix Allen Newell pour l'excellence en recherche du département d'informatique de l'Université Carnegie-Mellon[1].
- En 1999, il est corécipiendaire, avec Randal Bryant, E. Allen Emerson, et Kenneth McMillan (en) du prix Paris Kanellakis de l'ACM pour le développement du model checking symbolique[2].
- En 2004 il obtient le prix en mémoire de Harry H. Goode (en) de l'IEEE Computer Society « pour ses contributions importantes et pionnières à la vérification formelle des systèmes logiciels et matériels, et pour l'impact profond de ces contributions sur l'industrie électronique »[3].
- En 2005, il est élu membre de l'Académie nationale d'ingénierie des États-Unis pour ses contributions à la vérification formelle de la correction du logiciel et du matériel informatique.
- En 2008, il reçoit le prix Herbrand « en reconnaissance de son rôle dans l'invention du model checking et de son leadership constant dans ce domaine pendant plus de deux décennies ».
- En 2011, il est élu membre de l'Académie américaine des arts et des sciences.
Références
Liens externes
Sur les autres projets Wikimedia :
- Edmund M. Clarke, sur Wikimedia Commons
- Notices d'autorité
: - VIAF
- ISNI
- BnF (données)
- IdRef
- LCCN
- GND
- Pays-Bas
- Israël
- NUKAT
- Tchéquie
- WorldCat
- Ressources relatives à la recherche :
- Digital Bibliography & Library Project
- Google Scholar
- Mathematics Genealogy Project
- Scopus
- (en) Page personnelle à l'université Carnegie-Mellon
- (en) « Edmund Melson Clarke, Jr. », sur le site du Mathematics Genealogy Project
- Annonce prix Turing
- Site officiel du CMACS
Portail de l’informatique 
Portail des récompenses et distinctions 
Portail des États-Unis
