- Edmund Clarke
-
Edmund Melson Clarke, Jr. (* 27. Juli 1945) ist ein amerikanischer Informatiker und Turing-Preisträger. Zusammen mit Allen Emerson hat er Pionierarbeit auf dem Gebiet der Modellprüfung geleistet. Clarke ist Informatik-Professor an der Carnegie Mellon University.
Clarke studierte an der University of Virginia (Bachelor 1967) und der Duke University (Master 1968) Mathematik, danach Informatik an der Cornell University (Master 1974 und Ph. D. 1976).[1]
Danach lehrte er zunächst an der Duke University Informatik und ging 1978 als Assistenzprofessor nach Harvard. 1982 wechselte er an die Fakultät für Informatik der Carnegie Mellon University und wurde 1989 ordentlicher Professor.[2]
Clarke forscht insbesondere im Bereich der Software- und Hardware-Verifizierung und des maschinengestützten Beweisens. In seiner Dissertation bewies er, dass bestimmte Kontrollstrukturen von Programmiersprachen ihre Korrektheit nicht gut nach dem Hoare-Kalkül bewiesen. 1981 schlugen er und sein Doktorand Allen Emerson die Verwendung der Modellprüfung als Verifizierungstechnik für endliche parallele Systeme vor. Seine Forschungsgruppe verwendete die Modellprüfung erstmals zur Hardwareverifizierung. Auch die symbolische Modellprüfung mittels binärer Entscheidungsdiagramme wurde von seiner Gruppe entwickelt.[2]
2007 erhielt Clarke zusammen mit Emerson und dem unabhängig von den beiden ebenfalls an der Modellprüfung arbeitenden Joseph Sifakis den Turing Award. Daneben ist oder war Clarke Fellow der ACM, des IEEE, der Duke und der Cornell University und von IBM, und hat zahlreiche weitere Auszeichnungen erhalten, darunter der International Conference on VLSI Design Sidney Michaelson Best Paper Award 1991, der Semiconductor Research Corporation Technical Excellence Award 1995, der Carnegie Mellon Allen Newell Award for Excellence in Research 1999 (mit Emerson), der ACM Paris Kanellakis Award 1999 (mit Emerson, Randal Bryant und Kenneth L. McMillan) und der IEEE Harry H. Goode Memorial Award 2004. Er ist Mitglied von Sigma Xi und Phi Beta Kappa und wurde 2005 in die National Academy of Engineering gewählt.[1][2]
Clarke war Chefredakteur von Formal Methods in Systems Design und gehört den redaktionellen Beiräten mehrerer Zeitschriften an. Er hat mit Robert Kurshan, Amir Pnueli und Joseph Sifakis die International Conference on Computer Aided Verification gegründet und gehört deren und etlichen weiteren Programmkomitees an.[1]
Weblinks
Einzelnachweise
Personendaten NAME Clarke, Edmund Melson, Jr. KURZBESCHREIBUNG amerikanischer Informatiker und Turing-Preisträger GEBURTSDATUM 27. Juli 1945
Wikimedia Foundation.
