Die Laureaten

Copyright © Klaus Tschira Stiftung / Peter Badge

Edmund Melson Clarke

Turing-Award (2007) „zusammen mit E. Allen Emerson und Joseph Sifakis für ihre Rolle dabei, die Modellprüfung zu einer hocheffektiven Methode zur Verifikation werden zu lassen, die heute in der Hard- und Softwareindustrie breite Anwendung findet.“

Edmund M. Clarke studierte Mathematik, erst an der University of Virginia (Bachelor of Arts 1967), dann an der Duke University (Master of Arts 1968). Er promovierte anschließend in Informatik an der Cornell University (Ph.D. 1976). Er lehrte an der Duke University (1976-78) und an der Harvard University (1978-82). Seit 1982 gehört er zur Fakultät der Carnegie Mellon University. 1995 erhielt er als erster die FORE Systems Professorship, einen gut ausgestatteten Lehrstuhl an der School of Computer Science. Seit 2008 ist er University Professor.

Zusätzlich zum Turing-Preis erhielt Dr. Clarke zusammen mit anderen den ACM Kanellakis Award im Jahr 1998. 2004 erhielt Dr. Clarke den IEEE Harry H. Goode Memorial Award. Er wurde 2005 für seine Beiträge zur formalen Verifizierung von Hardware und Software in die National Academy of Engineering gewählt. Er erhielt 2008 den CADE Herbrand Award for Distinguished Contributions to Automated Reasoning und 2010 den LICS Test-of-Time Award. 2011 wurde er in die American Academy of Arts and Sciences gewählt. Er erhielt 2012 einen Ehrendoktortitel der Technischen Universität Wien. 2013 bekam er den Einstein Lehrstuhl der chinesischen Akademie der Wissenschaften.

Zu Dr. Clarkes Forschungsinteressen gehören die Verifizierung von Soft- und Hardware und das automatische Beweisen von Theoremen. 1981 schlugen er und E. Allen Emerson, einer seiner Doktoranden, erstmals vor, die Modellprüfung zu verwenden, um damit nebenläufige Programme zu verifizieren. Seine Forschungsgruppe an der Carnegie Mellon University war Vorreiter bei der Verwendung der Modellprüfung für die Verifizierung von Hard- und Software. Insbesondere entwickelte seine Gruppe die symbolische Modellprüfung mit Hilfe von binären Entscheidungsdiagrammen („Binary Decision Diagrams“, BDDs) sowie die beschränkte Modellprüfung mit schnellen SAT-Solvern und war führend im Gebrauch des CounterExample-Guided-Abstraction-Refinement (CEGAR). Zudem entwickelten Clarke und seine Studenten den ersten parallelen Theorembeweiser mit Resolutionskalkül („parallel general resolution theorem prover“, Parthenon) und den ersten Theorem-Beweiser, der auf symbolischen Berechnungen basierte (Analytica).

Bei der Modellprüfung werden Spezifikationen formuliert, die ein abstraktes Modell in einer Logik beschreiben, die zeitliche Aussagen erlaubt, etwa: „Sobald die Bremse gedrückt wird, wird das Fahrzeug langsamer“. Das abstrakte Modell ist einfach eine Formalisierung der Hardware und Software, die getestet werden sollen. Die Anfangszustände des Modells müssen die Formel erfüllen. Wenn sie das nicht tun, dann wird der Modellprüfer eine Kette von Gegenbeispielen finden, die zeigt, warum die Spezifizierung nicht erfüllt werden kann. Die Methode ermöglicht eine automatische Modellprüfung per Computer. So kann die Modellprüfung zum Beispiel die Korrektheit digitaler Schaltkreise oder des Synchronisierungs-Skeletts eines komplexen Programmes feststellen. Falls das Design einen Fehler enthält, dann kennzeichnet der Algorithmus die Situation, in der der Fehler auftritt und warnt den Nutzer, dass möglicherweise eine Korrektur nötig ist.