Edmund M. Clarke

Un article de Wikipedia, l'encyclopedie libre.
Page d’aide sur l’homonymie

Pour les articles homonymes, voir Clarke .

Edmund  M . Clarke
Edmund M. Clarke en 2006.
Biographie
Naissance
Deces
Nom dans la langue maternelle
Edmund Melson Clarke, Jr. Voir et modifier les données sur Wikidata
Nationalite
Formation
Activites
Autres informations
A travaille pour
Membre de
Directeur de these
Site web
Distinctions

modifier - modifier le code - modifier Wikidata Documentation du modèle

Edmund Melson Clarke, Jr. ( - ) est un informaticien universitaire connu pour ses contributions au model checking , une methode de verification de conceptions de logiciel et materiel. Il est titulaire de la chaire FORE Systems   (en) en informatique a l' universite Carnegie-Mellon . Clarke a ete l'un des trois recipiendaires, avec E. Allen Emerson et Joseph Sifakis , du prix Turing 2007, decerne par l' Association for Computing Machinery (ACM).

Biographie [ modifier | modifier le code ]

Clarke obtient un B.A. en mathematiques a l' universite de Virginie de Charlottesville en 1967, puis une maitrise (M.A.) en mathematiques a l' universite Duke de Durham (Caroline du Nord) en 1968, et un Ph.D. en informatique a l' universite Cornell , a Ithaca (New York) en 1976. Apres son Ph.D., il enseigne au departement d'informatique de l' universite Duke pendant deux ans, et en 1978 il part pour l' universite Harvard a Cambridge (Massachusetts) ou il est professeur assistant en informatique dans le departement d’ingenierie et de sciences appliquees. Apres Harvard, il rejoint en 1982 le departement d'informatique de l' universite Carnegie-Mellon a Pittsburgh . Il devient professeur titulaire en 1989. En 1995, il est le premier titulaire de la chaire FORE Systems   (en) , une chaire attachee a la Carnegie Mellon School of Computer Science   (en) .

Il est membre de la societe scientifique Sigma Xi et de l'association d'anciens eleves Phi Beta Kappa .

Œuvre [ modifier | modifier le code ]

Les interets scientifiques de Clarke comprennent la verification et la validation de logiciels et de materiels informatiques, et la demonstration automatique de theoremes .

Dans sa these de Ph.D., il montre que certaines structures de controle de langages de programmation ne possedent pas de bons systemes de preuve en logique de Hoare . En 1981, lui et son etudiant en Ph.D. Allen Emerson sont les premiers a proposer l'usage du model checking comme technique de verification pour des systemes concurrents a un nombre fini d'etats.

Son groupe de recherche est alors pionnier dans l'usage du model checking pour la verification du materiel . Le model checking symbolique, utilisant les diagrammes de decision binaire (ou BDD) est egalement developpe par son groupe. La these de Ph. D. de Kenneth McMillan developpe une technique importante de ce theme ; elle a obtenu le prix d'excellence des theses de l' ACM .

De plus, le groupe de recherche de Clarke a developpe le premier demonstrateur de theoremes parallele ( Parthenon ) et le premier demonstrateur de theoremes base sur un systeme de calcul symbolique ( Analytica ).

En 2009, il dirige la creation du centre CMACS (Computational Modeling and Analysis of Complex Systems), finance par la National Science Foundation . Ce centre comprend un groupe de chercheurs, repartis sur plusieurs universites, qui appliquent l' interpretation abstraite et le model checking aux systemes biologiques et aux systemes embarques.

Ouvrage [ modifier | modifier le code ]

Prix et distinctions [ modifier | modifier le code ]

References [ modifier | modifier le code ]

  1. ↑ Liste des recipiendaires sur le site de Carnegie-Mellon .
  2. ↑ Annonce sur le site de l'ACM .
  3. ↑ annonce sur le site de l'IEEE .

Liens externes [ modifier | modifier le code ]

Sur les autres projets Wikimedia :

v  · m
Laureats du prix Turing
Ce document provient de ≪  https://fr.wikipedia.org/w/index.php?title=Edmund_M._Clarke&oldid=211247990  ≫.