Edmund M. Clarke

Edmund M. Clarke
Edmund M. Clarke 2006

Edmund „Ed“ Melson Clarke, Jr. (* 27. Juli 1945 in Newport News, Virginia) 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.

Inhaltsverzeichnis

Leben

Clarke wuchs in Smithfield, Virginia, als Sohn eines Vertreters und einer Krankenschwester auf. Er 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. bei Robert Constable 1976 mit der Arbeit Completeness and Incompleteness Theorems for Hoare-like Axiom Systems).[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 erster Doktorand Allen Emerson die Verwendung der Modellprüfung als Verifizierungstechnik für endliche parallele Systeme vor, 1982 implementierte Edmund M. Clarke den ersten Modellprüfer EMC.

Clarkes Forschungsgruppe verwendete die Modellprüfung auch erstmals zur Hardwareverifizierung. Die symbolische Modellprüfung mittels binärer Entscheidungsdiagramme wurde ebenso von seiner Gruppe (um den Doktoranden Kenneth L. McMillan) entwickelt.[2]

Edmund 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] Unter anderem beriet er auch die Hardwarehersteller Bolt, Beranek and Newman, DEC, Fujitsu, Intel und Synopsys, und den Softwarehersteller Cadence Design Systems, und war für die Bell Laboratories tätig.

Clarke leitet auch ein multidisziplinares Zehn-Millionen-Dollar-Programm der National Science Foundation zur Gründung des Institute for Model Discovery and Exploration of Complex Systems. Dieses soll Modellprüfung und abstrakte Interpretation unter dem Schlagwort MCAI 2.0 kombinieren, um etwa Bauchspeicheldrüsenkrebs früher erkennen und Vorhofflimmern vorherzusagen zu lernen und sicherere Autos und Flugzeuge bauen zu können. An dem Projekt sind u.a. Amir Pnueli und James Glimm beteiligt.

Clarke ist verheiratet und hat drei Söhne.

Auszeichnungen

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), der IEEE Harry H. Goode Memorial Award 2004 und der Herbrand-Award 2008. Er ist Mitglied von Sigma Xi und Phi Beta Kappa und wurde 2005 in die National Academy of Engineering gewählt.[1][2]

Schriften

  • Mit Allen Emerson: Synthesis of synchronization skeletons for branching time temporal logic. In: Logic of Programs: Workshop, Yorktown Heights, NY, Mai 1981, Lecture Notes in Computer Science, Band 131, Springer-Verlag. 1981.
  • Mit J. R. Burch, Kenneth L. McMillan, David Dill und J. Hwang: Symbolic model checking: 10E20 states and beyond. In: LICS, 1990.

Weblinks

 Commons: Edmund M. Clarke – Sammlung von Bildern, Videos und Audiodateien

Einzelnachweise

  1. a b c Edmund M. Clarkes Curriculum Vitae, PDF
  2. a b c Edmund M. Clarkes Biographical Sketch

Wikimedia Foundation.

Игры ⚽ Нужен реферат?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Edmund M. Clarke — Saltar a navegación, búsqueda Edmund Melson Clarke, Jr. (*27 de julio de 1945) es un informático teórico estadounidense, principalmente reconocido por haber desarrollado el método conocido como model checking, para verificar diseños de software o …   Wikipedia Español

  • Edmund M. Clarke — Edmund Melson Clarke, Jr. (born July 27,1945) is a computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs.He is the FORE Systems Professor of Computer Science at Carnegie …   Wikipedia

  • 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… …   Deutsch Wikipedia

  • Edmund Lenihan — (born 1950), also known as Eddie Lenihan, is an Irish author, storyteller, lecturer and broadcaster. [cite book| last = Lenihan| first = Eddie| authorlink =| coauthors = Carolyn Eve Green| title = Meeting the Other Crowd | subtitle = The Fairy… …   Wikipedia

  • Clarke (Familienname) — Clarke ist ein englischer Familienname. Herkunft und Bedeutung Der Name ist eine Variante von Clark (neuenglisch clerk) und entspricht damit in etwa dem deutschen Namen Schreiber. Varianten Clark, Clerke Bekannte Namensträger Inhaltsverzeichnis A …   Deutsch Wikipedia

  • Clarke — Family name A scribe or clerk, the occupation from which the name derives Meaning Clerk, scribe, secretary …   Wikipedia

  • Clarke (surname) — This article is about surname Clarke. For other uses, see Clarke. Clarke Family name Meaning clerk Region of origin Ireland Related names Clark Clarke is an Irish surname from …   Wikipedia

  • Clarke (name) — Family name name =Clarke imagesize= caption= pronunciation = meaning = clerk region = Ireland origin = related names =Clark footnotes =Clarke is an Irish surname from County Galway that spread to County Donegal and County Dublin. The name is… …   Wikipedia

  • Edmund Kean — Saltar a navegación, búsqueda Edmund Kean interpretando a Sir Giles Overreach en la obra de Massinger A New Way to Pay Old Debts ( Nuevo modo de pagar antiguas deudas ), 1816 Edmund Kean (17 de marzo de 1787 – 15 de …   Wikipedia Español

  • Edmund Kean — (March 17, 1789 ndash; May 15, 1833) was an English actor, regarded in his time as the greatest ever. For many years he lived at Keydell House, Horndean.Early lifeKean was born in London. His father was probably Edmund Kean, an architect’s clerk …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”