Edmund M. Clarke
Edmund M. Clarke | |
|---|---|
 | |
| Geboren | Edmund Melson Clarke, Jr. 27. Juli 1945 Newport News, Virginia, UNS. |
| Gestorben | 22. Dezember 2020 (75 Jahre) |
| Staatsangehörigkeit | amerikanisch |
| Alma Mater | Cornell Universität |
| Bekannt für | Modellprüfung |
| Auszeichnungen | BIN. Turing Award |
| Wissenschaftliche Karriere | |
| Felder | Informatik |
| Institutionen | Carnegie Mellon Universität |
| These | Vollständigkeits- und Unvollständigkeitsmenge für Hoare-ähnliche Axiomsysteme (1976) |
| Doktorand | Robert Lee Constable |
| Doktorand | |
| Webseite | www |
Edmund Melson Clarke, Jr. (27. Juli 1945 - 22. Dezember 2020) war ein Amerikaner Informatiker und akademisch zur Entwicklung bekannt Modellprüfung, eine Methode zur offiziellen Überprüfung von Hardware- und Softwaredesigns. Er war der Vordersysteme Professor der Informatik bei Carnegie Mellon Universität. Clarke zusammen mit E. Allen Emerson und Joseph Sifakis, erhielt die 2007 ACM Turing Award.
Biografie
Clarke erhielt a B.A. Abschluss in Mathematik von dem Universität von Virginia, Charlottesville, VA, im Jahr 1967 ein M.A. Abschluss in Mathematik aus Duke University, Durham NC, im Jahr 1968 und a Ph.D. Abschluss in Informatik aus Cornell Universität, Ithaca ny 1976 unterrichtete er in der Abteilung für Informatik bei der Abteilung für Informatik Duke University, für zwei Jahre. 1978 zog er zu Harvard Universität, Cambridge, MA wo er Assistenzprofessor von war Informatik in dem Aufteilung der angewandten Wissenschaften. Er verließ Harvard 1982, um sich der Fakultät der Informatikabteilung beizumachen Carnegie Mellon Universität, Pittsburgh, PA. Er wurde 1989 zum vollständigen Professor ernannt. 1995 wurde er der erste Empfänger der Vordersysteme Professur, ein Stiftungsstuhl in der Carnegie Mellon School of Computer Science. Er wurde 2008 Universitätsprofessor und wurde 2015 emeritierter Professor.[2]
Er starb an COVID-19 im Dezember 2020 während der Covid-19-Pandemie in Pennsylvania.[3][4]
Arbeit
Clarkes Interessen eingeschlossen Software und Hardware- Überprüfung und automatischer Theorem -Beweis. In seiner Ph.D. These er hat das sicher bewiesen Programmiersprache Kontrollstrukturen hatten nicht gut Proof-Systeme im Hoare-Stil. 1981 Ph.D. Schüler E. Allen Emerson schlug zuerst die Verwendung von vor Modellprüfung als Überprüfungstechnik für endliche Zustand gleichzeitige Systeme. Seine Forschungsgruppe war der Einsatz von Pionierarbeit von Modellprüfung zum Hardwareüberprüfung. Symbolisch Modellprüfung Verwendung Binäre Entscheidungsdiagramme wurde auch von seiner Gruppe entwickelt. Diese wichtige Technik war Gegenstand von Kenneth McMillans Ph.D. These, die eine erhielt ACM Doktorand Dissertation Vergeben. Darüber hinaus entwickelte seine Forschungsgruppe die erste parallele Auflösung Theorem Prover (Parthenon) und der erste Theorem -Prover, der auf einem symbolischen Berechnungssystem (Analytica) basiert. Im Jahr 2009 leitete er die Erstellung des Computermodellierung und Analyse des CMACS -Zentrums (COMACS), das von der finanziert wird Nationale Wissenschaftsstiftung. Dieses Zentrum verfügt über ein Forscherteam, das mehrere Universitäten umfasst, sich bewerben Abstrakte Interpretation und Modellprüfung zu biologischen und eingebetteten Systemen.
Professionelle Anerkennung
Clarke war a Gefährte des ACM und die IEEE. Er erhielt einen technischen Exzellenzpreis von der Semiconductor Research Corporation im Jahr 1995 und ein Allen Newell Auszeichnung für Exzellenz in der Forschung aus dem Carnegie Mellon Informatik Abteilung im Jahr 1999. Er war Co-Gewinner zusammen mit Randal Bryant, E. Allen Emersonund Kenneth McMillan vom ACM Paris Kanellakis Award im Jahr 1999 für die Entwicklung von Symbolische Modellprüfung. 2004 erhielt er das IEEE Computer Society Harry H. Goode Memorial Award für bedeutende und wegweisende Beiträge zur formellen Überprüfung von Hardware- und Softwaresystemen sowie für die tiefgreifenden Auswirkungen, die diese Beiträge zur Elektronikbranche geleistet haben. Er wurde in die gewählt Nationale Akademie des Ingenieurwesens Im Jahr 2005 für Beiträge zur formalen Überprüfung der Hardware und der Korrektheit der Software. Er wurde in die gewählt Amerikanische Akademie für Kunst und Wissenschaften im Jahr 2011. Er erhielt das Herbrand Award 2008 in "Anerkennung seiner Rolle bei der Erfindung der Modellprüfung und seiner anhaltenden Führung in der Region seit mehr als zwei Jahrzehnten". Er erhielt die 2014 Bower Award und Preis für Leistungen in der Wissenschaft von dem Franklin Institute Für "seine Hauptrolle bei der Konzeption und Entwicklung von Techniken zur automatischen Überprüfung der Richtigkeit einer breiten Palette von Computersystemen, einschließlich derjenigen, die in Transport, Kommunikation und Medizin zu finden sind". Er war Mitglied von Sigma XI und Phi Beta Kappa.
Siehe auch
Verweise
- ^ Edmund Melson Clarke, Jr.
- ^ "Edmund M. Clarke". Cs.cmu.edu. Abgerufen 24. Dezember 2020.
- ^ James S. Clarke [@jim_in_oregon] (22. Dezember 2020). "Mein Vater, Edmund M Clarke, ist heute aus Covid verstorben. [...]" (Tweet) - über Twitter.
- ^ "Edmund Clarke war Pioniermethoden zur Erkennung von Software, Hardwarefehler | Carnegie Mellon School of Computer Science". Cs.cmu.edu. Abgerufen 24. Dezember 2020.