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