Edmund M. Clarke - Edmund M. Clarke
Edmund M. Clarke | |
|---|---|
 | |
| Født |
Edmund Melson Clarke, Jr.
27. juli 1945
Newport News, Virginia , USA
|
| Døde | 22. desember 2020 (75 år)
Pittsburgh , Pennsylvania , USA
|
| Nasjonalitet | amerikansk |
| Alma mater | Cornell University |
| Kjent for | Modellkontroll |
| Utmerkelser | AM Turing Award |
| Vitenskapelig karriere | |
| Enger | Informatikk |
| Institusjoner | Carnegie Mellon University |
| Avhandling | Fullstendighet og ufullstendighetssetninger for Hoare-lignende aksiomsystemer (1976) |
| Doktorgradsrådgiver | Robert Lee Konstabel |
| Doktorgradsstudenter | |
| Nettsted | www |
Edmund Melson Clarke, Jr. (27. juli 1945 - 22. desember 2020) var en amerikansk informatiker og akademiker kjent for å ha utviklet modellkontroll , en metode for å formelt verifisere maskinvare- og programvaredesign. Han var FORE Systems Professor i informatikk ved Carnegie Mellon University . Clarke, sammen med E. Allen Emerson og Joseph Sifakis , mottok 2007 ACM Turing Award .
Biografi
Clarke mottok en BA -grad i matematikk fra University of Virginia , Charlottesville, VA , i 1967, en MA -grad i matematikk fra Duke University , Durham NC , i 1968 og en doktorgrad. grad i informatikk fra Cornell University , Ithaca NY i 1976. Etter å ha mottatt sin doktorgrad, underviste han ved Institutt for informatikk ved Duke University i to år. I 1978 flyttet han til Harvard University , Cambridge, MA, hvor han var assisterende professor i informatikk i avdelingen for anvendt vitenskap . Han forlot Harvard i 1982 for å bli med på fakultetet i datavitenskapelig avdeling ved Carnegie Mellon University , Pittsburgh, PA . Han ble utnevnt til professor i 1989. I 1995 ble han den første mottakeren av FORE Systems Professorship, en begavet stol ved Carnegie Mellon School of Computer Science . Han ble universitetsprofessor i 2008 og ble emeritusprofessor i 2015. Han døde av COVID-19 under COVID-19-pandemien i Pennsylvania i 2020.
Arbeid
Clarke interesser inkludert programvare og maskinvare verifikasjon og automatisk teorembevis . I sin doktorgrad avhandlingen beviste han at visse programmeringsspråklige kontrollstrukturer ikke hadde gode systemer i Hoare -stil . I 1981 han og hans doktorgrad. student E. Allen Emerson foreslo først bruk av modellkontroll som verifikasjonsteknikk for endelige tilstands samtidige systemer . Forskningsgruppen hans var banebrytende for bruk av modellkontroll for maskinvareverifisering . Symbolsk modellkontroll ved bruk av binære beslutningsdiagrammer ble også utviklet av gruppen hans. Denne viktige teknikken var gjenstand for Kenneth McMillans Ph.D. avhandling, som mottok en ACM Doctoral Dissertation Award. I tillegg utviklet forskningsgruppen hans den første parallelle oppløsningen teorem prover (Parthenon) og den første teoremprover som var basert på et symbolsk beregningssystem (Analytica). I 2009 ledet han etableringen av senteret Computational Modeling and Analysis of Complex Systems (CMACS), finansiert av National Science Foundation . Dette senteret har et team av forskere som strekker seg over flere universiteter og bruker abstrakt tolkning og modellkontroll på biologiske og innebygde systemer.
Profesjonell anerkjennelse
Clarke var stipendiat i ACM og IEEE . Han mottok en Technical Excellence Award fra Semiconductor Research Corporation i 1995 og en Allen Newell Award for Excellence in Research fra Carnegie Mellon Computer Science Department i 1999. Han var en medvinner sammen med Randal Bryant , E. Allen Emerson og Kenneth McMillan fra ACM Paris Kanellakis Award i 1999 for utvikling av symbolsk modellkontroll . I 2004 mottok han IEEE Computer Society Harry H. Goode Memorial Award for betydelige og banebrytende bidrag til formell verifikasjon av maskinvare- og programvaresystemer, og for den store innvirkningen disse bidragene har hatt på elektronikkindustrien. Han ble valgt til National Academy of Engineering i 2005 for bidrag til den formelle verifiseringen av maskinvare og programvarens korrekthet. Han ble valgt til American Academy of Arts and Sciences i 2011. Han mottok Herbrand -prisen i 2008 i "anerkjennelse av sin rolle i oppfinnelsen av modellkontroll og hans vedvarende lederskap i området i mer enn to tiår." Han mottok 2014 Bower Award og prisen for prestasjon i vitenskap fra Franklin Institute for "sin ledende rolle i utformingen og utviklingen av teknikker for automatisk å verifisere korrektheten til et bredt spekter av datasystemer, inkludert de som finnes innen transport, kommunikasjon og medisin." Han var medlem av Sigma Xi og Phi Beta Kappa .