에드먼드 M. 클라크

Edmund M. Clarke
에드먼드 M. 클라크
Edmund Clarke FLoC 2006.jpg
태어난
에드먼드 멜슨 클라크 주니어

(1945-07-27)1945년 7월 27일
뉴포트 뉴스, 버지니아, 미국
죽은2020년 12월 22일(2020-12-22) (75세)
미국 [1]펜실베니아 주 피츠버그
국적.아메리칸
모교코넬 대학교
로 알려져 있다모델 체크
어워드A.M. 튜링상
과학 경력
필드컴퓨터 공학
기관카네기 멜론 대학교
논문Hoare-like Axiom 시스템의 완전성과 불완전성 이론 (1976)
박사 어드바이저로버트 리 컨스터블
박사과정 학생
웹 사이트www.cs.cmu.edu/~http://filename

에드먼드 멜슨 클라크 주니어(Edmund Melson Clarke, Jr., 1945년 7월 27일 ~ 2020년 12월 22일)는 미국의 컴퓨터 과학자이자 학자로 하드웨어 및 소프트웨어 설계를 공식적으로 검증하는 방법인 모델 체크를 개발한 것으로 알려져 있습니다.그는 카네기 멜론 대학의 FORE 시스템즈 교수였습니다.클라크, E와 함께. Allen Emerson과 Joseph Sifakis는 2007년 ACM Turing Award를 받았습니다.

전기

클라크는 1967년 버지니아주 샬로츠빌에서 수학 학사 학위를, 1968년 듀크대 더럼 NC에서 수학 석사 학위를, 1976년 코넬대 이타카 NY에서 컴퓨터 과학 박사 학위를 받았습니다.박사학위를 받은 후, 그는 듀크 대학의 컴퓨터 과학부에서 2년 동안 가르쳤다.1978년, 그는 하버드 대학교, 캠브리지, 매사추세츠로 이사하여 응용과학부의 컴퓨터 과학 조교수로 재직했습니다.그는 1982년 하버드를 떠나 펜실베이니아주 피츠버그에 있는 카네기 멜론 대학의 컴퓨터 과학부에 들어갔다.그는 1989년에 정교수로 임명되었습니다.1995년, 그는 카네기 멜론 컴퓨터 사이언스 스쿨의 기부 교수인 FORE 시스템즈 교수의 첫 수상자가 되었습니다.그는 2008년에 대학교수가 되었고 [2]2015년에 명예 교수가 되었다.

그는 2020년 12월 [3][4]펜실베니아에서 COVID-19 대유행 중 COVID-19로 사망했다.

일하다.

Clarke의 관심사는 소프트웨어와 하드웨어 검증과 자동 정리 증명이었습니다.박사학위 논문에서 그는 특정 프로그래밍 언어 제어 구조가 호어 스타일의 좋은 증명 시스템을 가지고 있지 않다는 것을 증명했다.1981년 그와 그의 박사과정 학생 E. Allen Emerson은 처음에 유한 상태 동시 시스템의 검증 기법으로 모델 체크를 사용할 것을 제안했다.그의 연구 그룹은 하드웨어 검증을 위한 모델 체크의 사용을 개척했습니다.이항 결정도를 이용한 상징적 모델 확인 또한 그의 그룹에 의해 개발되었다.이 중요한 기술은 ACM 박사논문상을 받은 케네스 맥밀런의 박사학위 논문의 주제였다.게다가, 그의 연구 그룹은 기호 계산 시스템에 기초하는 최초의 병렬 분해능 정리 계산기(Parthenon)와 최초의 정리 계산기(Analytica)를 개발했다.2009년에는 National Science Foundation의 자금 지원을 받아 Computational Modeling and Analysis of Complex Systems(CMACS) 센터를 설립했습니다.이 센터에는 여러 대학에 걸친 연구팀이 있으며, 생물학적 시스템과 임베디드 시스템에 추상적 해석과 모델 체크를 적용하고 있습니다.

전문가로서의 인정

클라크는 ACM과 IEEE의 펠로우였다.그는 1995년 반도체 리서치 코퍼레이션으로부터 테크니컬 엑설런스 어워드, 1999년 카네기 멜론 컴퓨터 과학부에서 앨런 뉴웰 어워드 연구 우수상을 받았습니다.그는 1999년 상징적인 모델 체크의 개발로 ACM 파리 카넬라키스의 랜달 브라이언트, E. 앨런 에머슨, 케네스 맥밀런과 함께 공동 수상자였다.2004년에는 하드웨어 및 소프트웨어 시스템의 정식 검증에 대한 중요한 선구적 공헌과 이러한 공헌이 전자산업에 미치는 지대한 영향을 인정받아 IEEE Computer Society H. Goode Memorial Award를 수상했습니다.그는 2005년에 하드웨어와 소프트웨어의 정확성을 공식적으로 검증하는 데 기여한 공로로 미국 공학 아카데미에 선출되었습니다.그는 2011년 미국 예술 과학 아카데미 회원으로 선출되었다.그는 2008년 "모델 체크 발명에 대한 자신의 역할과 20년 이상 이 지역에서 지속된 리더십을 인정받아"에서 허브랜드상을 받았다.그는 "교통, 통신, 의학을 포함한 광범위한 컴퓨터 시스템의 정확성을 자동으로 검증하는 기술의 개념과 개발에서 주도적인 역할을 한 공로로 프랭클린 연구소로부터 2014 바우어 상과 과학 공로상을 받았다.그는 Sigma Xi와 Phi Beta Kappa의 멤버였다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ 에드먼드 멜슨 클라크 주니어
  2. ^ "Edmund M. Clarke". Cs.cmu.edu. Retrieved 24 December 2020.
  3. ^ James S. Clarke [@Jim_in_Oregon] (22 December 2020). "My father, Edmund M Clarke, passed away from Covid today. [...]" (Tweet) – via Twitter.
  4. ^ "Edmund Clarke Pioneered Methods For Detecting Software, Hardware Errors Carnegie Mellon School of Computer Science". Cs.cmu.edu. Retrieved 24 December 2020.

외부 링크

Wikimedia Commons에는 Edmund M. Clarke와 관련된 미디어가 있습니다.