Edmund M. Clarke

Edmund M. Clarke Bilde i infoboks. Edmund M. Clarke i 2006. Biografi
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
Annen informasjon
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).  

Biografi

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 .

Kunstverk

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.

Arbeid

Priser og anerkjennelse

Referanser

  1. Liste over mottakere på Carnegie-Mellon-siden .
  2. Kunngjøring på ACMs nettsted .
  3. kunngjøring på IEEE-nettstedet .

Eksterne linker