Edmund M. Clarke - Edmund M. Clarke
Edmund M. Clarke | |
|---|---|
 | |
| Doğmak |
Edmund Melson Clarke, Jr.
27 Temmuz 1945 |
| Öldü | 22 Aralık 2020 (75 yaşında)
Pittsburgh , Pensilvanya , ABD
|
| Milliyet | Amerikan |
| gidilen okul | Cornell Üniversitesi |
| Bilinen | Model kontrolü |
| Ödüller | AM Turing Ödülü |
| Bilimsel kariyer | |
| Alanlar | Bilgisayar Bilimi |
| kurumlar | Carnegie Mellon Üniversitesi |
| Tez | Hoare-Benzeri Aksiyom Sistemleri İçin Tamlık ve Eksiklik Teoremleri (1976) |
| Doktora danışmanı | Robert Lee Memur |
| Doktora öğrencileri | |
| İnternet sitesi | www |
Edmund Melson Clarke, Jr. (27 Temmuz 1945 - 22 Aralık 2020), donanım ve yazılım tasarımlarını resmi olarak doğrulamak için bir yöntem olan model kontrolü geliştirmesiyle tanınan Amerikalı bir bilgisayar bilimcisi ve akademisyeniydi . Öyleydi FORE Sistemleri Profesörü Bilgisayar Bilimleri at Carnegie Mellon Üniversitesi . Clarke, E. Allen Emerson ve Joseph Sifakis ile birlikte 2007 ACM Turing Ödülü'nü aldı .
biyografi
Clarke alınan BA derecesini matematik gelen Virjinya Üniversitesi , Charlottesville , 1967 yılında, bir MA derecesini matematik gelen Duke Üniversitesi'nde , Durham NC 1968 yılında, ve Doktora derecesi Bilgisayar Bilimleri gelen Cornell Üniversitesi , Ithaca NY 1976 yılında doktorasını aldıktan sonra, Bilgisayar Bilimleri Bölümü öğretilen Duke Üniversitesi'nde iki yıl boyunca,. 1978'de Harvard Üniversitesi , Cambridge, MA'ya taşındı ve burada Uygulamalı Bilimler Bölümü'nde Bilgisayar Bilimleri alanında Yardımcı Doçent oldu . O Computer Science Bölümünde öğretim katılmak üzere 1982 yılında Harvard sol Carnegie Mellon Üniversitesi , Pittsburgh, PA . 1989'da Tam Profesör olarak atandı. 1995'te Carnegie Mellon Bilgisayar Bilimleri Okulu'nda bahşedilmiş bir kürsü olan FORE Systems Profesörlüğünün ilk sahibi oldu . 2008'de Üniversite Profesörü oldu ve 2015'te fahri profesör oldu. 2020'de Pennsylvania'da COVID-19 salgını sırasında COVID-19'dan öldü .
Çalışmak
Clarke'ın ilgi alanları arasında yazılım ve donanım doğrulaması ve otomatik teorem ispatı vardı . Doktora derecesinde bazı programlama dili kontrol yapılarının iyi Hoare tarzı kanıtlama sistemlerine sahip olmadığını kanıtladı . 1981 yılında o ve doktorası öğrenci E. Allen Emerson, ilk olarak, sonlu durumlu eşzamanlı sistemler için bir doğrulama tekniği olarak model kontrolünün kullanılmasını önerdi . Araştırma grubu , donanım doğrulaması için model kontrolünün kullanılmasına öncülük etti . İkili karar diyagramlarını kullanarak sembolik model kontrolü de onun grubu tarafından geliştirilmiştir. Bu önemli teknik, Kenneth McMillan'ın Ph.D.'sinin konusuydu. ACM Doktora Tezi Ödülü alan tez . Ayrıca, onun araştırma grubu, ilk paralel çözünürlük teorem ispatlayıcısını (Parthenon) ve sembolik bir hesaplama sistemine (Analytica) dayanan ilk teorem ispatlayıcısını geliştirdi. 2009 yılında Ulusal Bilim Vakfı tarafından finanse edilen Kompleks Sistemlerin Hesaplamalı Modellenmesi ve Analizi (CMACS) merkezinin oluşturulmasına öncülük etti . Bu merkez, birden fazla üniversiteyi kapsayan, biyolojik ve gömülü sistemlere soyut yorumlama ve model kontrolü uygulayan bir araştırmacı ekibine sahiptir .
Profesyonel tanınma
Clarke oldu dost ve ACM ve IEEE . 1995'te Semiconductor Research Corporation'dan Teknik Mükemmellik Ödülü ve 1999'da Carnegie Mellon Bilgisayar Bilimleri Departmanından Allen Newell Araştırmada Mükemmellik Ödülü aldı. Randal Bryant , E. Allen Emerson ve Kenneth ile birlikte ortak kazanan oldu. McMillan , sembolik model kontrolünü geliştirdiği için 1999'da ACM Paris Kanellakis Ödülü'ne layık görüldü . 2004 yılında donanım ve yazılım sistemlerinin resmi doğrulamasına önemli ve öncü katkıları ve bu katkıların elektronik endüstrisi üzerindeki derin etkisi nedeniyle IEEE Computer Society Harry H. Goode Memorial Ödülü'nü aldı. Donanım ve yazılım doğruluğunun resmi olarak doğrulanmasına katkılarından dolayı 2005 yılında Ulusal Mühendislik Akademisi'ne seçildi . 2011'de Amerikan Sanat ve Bilim Akademisi'ne seçildi . 2008'de "model kontrolünün icadındaki rolünün tanınması ve bölgede yirmi yıldan fazla süredir devam eden liderliği" nedeniyle Herbrand Ödülü'nü aldı . O 2014 Alınan Bilimleri Başarı Bower Ödülü ve Ödülü gelen Franklin Institute otomatik ulaşım, haberleşme olanlar, bulan dahil bilgisayar sistemlerinin geniş bir dizi doğruluğunu doğrulamak için tekniklerinin kavranması ve geliştirilmesi konusunda üstlendiği öncü rolü" için, ve ilaç." O bir üyesiydi Sigma Xi ve Phi Beta Kappa .