Fødsel |
27. juli 1945 Newport News |
---|---|
Død |
22. desember 2020(75 år gammel) Pittsburgh |
Navn på morsmål | Edmund Melson Clarke, Jr. |
Nasjonalitet | amerikansk |
Opplæring |
University of Virginia (1967) Duke University (1968) Cornell University (1976) |
Aktiviteter | Informatiker , universitetsprofessor , forsker , ingeniør , matematiker |
Jobbet for | Carnegie-Mellon University , Duke University (1976) , Harvard University (1978) , Cornell University (1982) |
---|---|
Områder | Informasjonsvitenskap ( in ) , datamaskin |
Medlem av |
Institute of Electrical and Electronics Engineers Association for Computing Machinery United States National Academy of Engineering (2005) American Academy of Arts and Sciences (2011) |
Veileder | Robert lee konstabel |
Nettsted | (no) www.cs.cmu.edu/~emc |
Utmerkelser |
Turing-prisen (2007) |
Edmund Melson Clarke, Jr. (27. juli 1945 - 22. desember 2020) er en akademisk informatiker kjent for sine bidrag til modellkontroll , en metode for å verifisere programvare- og maskinvaredesign. Han har stolen FORE Systems (in) i IT ved Carnegie-Mellon University . Clarke var en av tre mottakere, sammen med E. Allen Emerson og Joseph Sifakis , av 2007 Turing-prisen , tildelt av Association for Computing Machinery (ACM).
Clarke tok en BA i matematikk fra University of Virginia i Charlottesville i 1967, deretter en mastergrad (MA) i matematikk fra Duke University i Durham (North Carolina) i 1968, og en doktorgrad i informatikk fra ' Cornell University , i Ithaca (New York) i 1976. Etter doktorgraden lærte han ved iT-avdelingen ved Duke University i to år, og i 1978 dro han til Harvard University i Cambridge (Massachusetts) hvor han er assisterende professor i informatikk ved avdelingen. av ingeniørfag og anvendt vitenskap. Etter Harvard, i 1982, begynte han i informatikkavdelingen ved Carnegie-Mellon University i Pittsburgh . Han ble professor i 1989. I 1995 ble han den første innehaveren av stolen FORE Systems (i) en stol knyttet til Carnegie Mellon School of Computer Science (in) .
Han er medlem av Sigma Xi Scientific Society og av Phi Beta Kappa Alumni Association .
Clarkes vitenskapelige interesser inkluderer verifisering og validering av programvare og maskinvare, og automatisk demonstrasjon av teoremer .
I sin doktorgradsavhandling viser han at noen kontrollstrukturer for programmeringsspråk ikke har gode proofsystemer i Hoare-logikken . I 1981 var han og doktorgradsstudenten Allen Emerson den første som foreslo bruken av modellkontroll som en verifiseringsteknikk for systemer samtidig med et begrenset antall stater.
Forskningsgruppen hans var da en pioner innen bruk av modellkontroll for å sjekke utstyr . Den modell kontroll symbolsk ved hjelp av de binære beslutningsdiagrammene (eller BDD) er også utviklet av hans gruppe. Kenneth McMillans doktoravhandling utvikler en viktig teknikk for dette temaet; hun mottok avhandlingens utmerkelsespris fra ACM .
I tillegg, Clarke forskergruppe utviklet den første parallell teorem prøveapparat ( Parthenon ) og den første teoremet prove basert på en symbolsk kalkulus system ( Analytica ).
I 2009 ledet han etableringen av senteret CMACS (Computational Modelling and Analysis of Complex Systems), finansiert av National Science Foundation . Dette senteret inkluderer en gruppe forskere, spredt over flere universiteter, som bruker abstrakt tolkning og modellkontroll på biologiske systemer og innebygde systemer.