Der Turing Award wurde Edmund M. Clarke im Jahr 2007 für seine bahnbrechende Entwicklung des Model Checking verliehen, einer formalen Verifizierungsmethode für Hardware- und Softwaredesigns. Seine Arbeit etablierte rigorose mathematische Techniken zur Sicherstellung der Korrektheit komplexer elektronischer Systeme und veränderte während seiner langen akademischen Laufbahn grundlegend die Art und Weise, wie Ingenieure die Zuverlässigkeit moderner Computerinfrastrukturen angehen.
Akademischer Werdegang
Clarke wurde 1945 in Newport News geboren und verfolgte einen traditionellen Weg über die Mathematik, bevor er zur Informatik wechselte. Er erwarb 1967 einen B.A. in Mathematik an der University of Virginia, gefolgt von einem M.A. an der Duke University im Jahr 1968. Seine formale Ausbildung schloss er 1976 mit einem Ph.D. in Informatik an der Cornell University ab, wo seine Abschlussarbeit kritische Einschränkungen in bestehenden Hoare-artigen Beweissystemen für Programmiersprachen-Kontrollstrukturen aufzeigte.
Berufliche Laufbahn
Clarke hatte Positionen an mehreren großen Institutionen inne, bevor er sich an der Carnegie Mellon University niederließ. Nach seiner Promotion lehrte er zwei Jahre lang an der Duke University und wechselte 1978 als Assistenzprofessor an die Harvard University. 1982 trat er in die Informatikfakultät der Carnegie Mellon ein. Er erhielt 1989 eine volle Professur und wurde 1995 zum ersten FORE Systems Professor ernannt. Im Jahr 2015 wechselte er in den Emeritus-Status.
Beiträge zur formalen Verifizierung
Im Jahr 1981 führten Clarke und sein Student E. Allen Emerson das Model Checking ein, eine Technik zur Verifizierung endlicher, nebenläufiger Systeme. Seine Forschungsgruppe leistete anschließend Pionierarbeit bei Hardware-Verifizierungsmethoden und symbolischem Model Checking unter Verwendung von binären Entscheidungsdiagrammen. Über diese Kernbemühungen hinaus entwickelte sein Team den Parthenon-Theorembeweiser für parallele Auflösung und das symbolische Berechnungssystem Analytica. Im Jahr 2009 gründete er das Zentrum für computergestützte Modellierung und Analyse komplexer Systeme, um diese Methoden auf biologische und eingebettete Systeme anzuwenden.
Zwanzig Fragen, acht Minuten auf der Uhr und ein Perzentil, gemessen an allen bisherigen Teilnehmern. Ohne Anmeldung.
IQ-Test starten →Berufliche Anerkennung
Clarkes Forschung brachte ihm zahlreiche Auszeichnungen ein, darunter den Paris Kanellakis Award 1998, den Harry H. Goode Memorial Award 2004 und den Herbrand Award 2008. Er wurde 2005 in die National Academy of Engineering und 2011 in die American Academy of Arts and Sciences gewählt. Im Jahr 2014 erhielt er den Bower Award and Prize for Achievement in Science vom Franklin Institute für seine Führung bei der automatisierten Systemverifizierung.
Fakten auf einen Blick
- Geboren: 1945, Newport News - Gestorben: 2020, Pittsburgh - Ausbildung: University of Virginia (1967), Duke University (1968), Cornell University (1976) - Hauptfach: Informatik - Wichtige Anerkennung: 2007 ACM Turing Award - Zugehörigkeiten: ACM, IEEE, National Academy of Engineering - Akademische Heimat: Carnegie Mellon University
Häufig gestellte Fragen
### Was ist Model Checking?
Es ist eine formale Verifizierungstechnik, die von Clarke und E. Allen Emerson entwickelt wurde, um die Korrektheit von Hardware- und Softwaredesigns sicherzustellen.
### Hatte Clarke einen Stiftungslehrstuhl inne?
Ja, er war der erste Inhaber der FORE Systems Professur an der Carnegie Mellon University, beginnend im Jahr 1995.
