Edmund M. Clarke

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Edmund M. Clarke en 2006

Edmund Melson Clarke, Jr. (né le 27 juillet 1945) est un informaticien universitaire connu pour ses développements du 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 est un des trois récipiendaires, avec E. Allen Emerson et Joseph Sifakis, du Prix Turing 2007, délivré par l'Association for Computing Machinery (ACM).

Biographie[modifier | modifier le code]

Clarke obtient un baccalauréat universitaire ès lettres (B.A.) en mathématiques de l'université de Virginie, à Charlottesville en 1967, puis une maîtrise universitaire ès lettres (M.A.) en mathématiques de l'université Duke, à Durham (Caroline du Nord) en 1968, et un Philosophiæ doctor (Ph.D.) en informatique de l'université Cornell, à Ithaca (New York) en 1976. Après son Ph.D., il enseigne au département d'informatique de l'Duke University 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 199. 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é de recherche scientifique Sigma Xi (en) et de l'association d'anciens élèves Phi Beta Kappa.

Œuvre[modifier | modifier le code]

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 bon systèmes de preuve en logique de Hoare. En 1981, lui et sont é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 pionnière pour l'usage du model checking pour la vérification du hardware. Le model checking symbolique, utilisant les diagrammes de décision binaire (ou BDDs) également est développé par son groupe. Un technique importante a constitué le sujet de la thèse de Ph. D. de Kenneth McMillan qui a obtenu le prix d'excellece de la thèse de doctorat de l'ACM.

De plus, son groupe de recherche 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, couvrant de multiples universités, qui appliquent l'interprétation abstraite et le model checking aux systèmes biologiques et aux systèmes embarqués.

Ouvrage[modifier | modifier le code]

  • (en) Edmund M. Clarke, Orna Grumberg et Doron A. Peled, Model Checking, The MIT Press,‎ 1999 (ISBN 9780262032704)

Prix et distinctions[modifier | modifier le code]

  • En 2004 il obtient le Prix en mémoire de Harry H. Goode (en) de l'IEEE Computer Society « pour ses contribution 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].

Sur les autres projets Wikimedia :

Liens externes[modifier | modifier le code]

Références[modifier | modifier le code]

  1. Liste des récipiendaires sur le site de Carnegie-Mellon.
  2. Annonce sur le site de l'ACM.
  3. annonce sur le site de l'IEEE.