Edmund M. Clarke

Edmund „Ed“ Melson Clarke, Jr. (* 27. Juli 1945 in Newport News, Virginia; † 22. Dezember 2020 in Mt. Lebanon, Pennsylvania) war ein US-amerikanischer Informatiker. Zusammen mit Allen Emerson hat er Pionierarbeit auf dem Gebiet der Modellprüfung geleistet und wurde dafür 2007 mit dem Turing Award ausgezeichnet. Clarke war Informatik-Professor an der Carnegie Mellon University.

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 forschte insbesondere im Bereich der Software- und Hardware-Verifizierung und des maschinengestützten Beweisens. In seiner Dissertation bewies er, dass die Korrektheit bestimmter Kontrollstrukturen von Programmiersprachen nicht gut mit dem Hoare-Kalkül zu beweisen sind. 1981 schlugen er und sein erster Doktorand Allen Emerson die Verwendung der Modellprüfung (Model Checking) 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örte 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 leitete auch ein multidisziplinäres 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 waren u. a. Amir Pnueli und James Glimm beteiligt.

Vom 11. bis 14. Juni 2015 nahm er an der 63. Bilderberg-Konferenz in Telfs-Buchen in Österreich teil.

Clarke war verheiratet und hat drei Söhne.

Während der COVID-19-Pandemie in den Vereinigten Staaten starb Clarke am 22. Dezember 2020 im Alter von 75 Jahren an den Folgen einer SARS-CoV-2-Infektion im Krankenhaus Asbury Heights in Mt. Lebanon.^[3][4]

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, der Herbrand Award 2008 und der Bower Award and Prize for Achievement in Science 2014. Er ist Mitglied von Sigma Xi und Phi Beta Kappa und wurde 2005 in die National Academy of Engineering gewählt,^[1][2] 2011 in die American Academy of Arts and Sciences. 2012 erhielt er ein Ehrendoktorat der Technischen Universität Wien.^[5][6]

• 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.
• Mit Orna Grumberg und Doron A. Peled: Model Checking. MIT Press, 1999.
• Mit Allen Emerson und Joseph Sifakis: Model Checking. Algorithmic verification and debugging in: Commun. ACM Volume 52, No. 11 (November 2009), 74–84 (Turing-Vorlesung der Preisträger des 2007 ACM A.M. Turing Award).

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

• Clarkes Website bei der Carnegie Mellon University (englisch)
• Model Checking’s Role Model (PDF; 1,7 MB), The Link, Ausgabe 4.1, Sommer 2009, S. 8–11, ausführlicher Bericht zu Clarkes Einfluss auf seine Studenten, mit privaten Fotos (englisch)

1. ↑ ^{a b c} Edmund M. Clarkes Curriculum Vitae, PDF
2. ↑ ^{a b c} Edmund M. Clarkes Biographical Sketch
3. ↑ Andrew Goldstein: Obituary: Edmund M. Clarke, CMU professor who won computer science’s Nobel Prize equivalent, post-gazette.com, abgerufen am 25. Dezember 2020.
4. ↑ Simson Garfunkel, Eugene H. Spafford: In Memoriam Edmund M. Clarke (1945–2020) in: Commun. ACM Volume 64 No. 03 (März 2021).
5. ↑ TU Wien: Ehre wem Ehre gebührt!. Artikel vom 26. Jänner 2015, abgerufen am 26. März 2015.
6. ↑ TU Wien: Ehrendoktorate (Memento vom 21. Februar 2016 im Internet Archive). Abgerufen am 26. März 2015.