에드먼드 M. 클라크
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.
1. 개요
에드먼드 M. 클라크는 소프트웨어 및 하드웨어 검증과 자동 정리 증명 분야에 기여한 컴퓨터 과학자이다. 버지니아 대학교에서 학사, 듀크 대학교에서 석사 학위를 받았으며 코넬 대학교에서 컴퓨터 과학 박사 학위를 취득했다. 듀크 대학교, 하버드 대학교, 카네기 멜론 대학교에서 교수로 재직했으며, 2007년 튜링상을 수상했다. 클라크는 모델 검증 기술을 개발하고, 기호적 모델 검증, 자동 정리 증명기 개발에 기여했으며, 2020년 코로나19로 사망했다.
더 읽어볼만한 페이지
- 카네기 멜런 대학교 교수 - 허버트 사이먼
허버트 사이먼은 제한된 합리성 개념을 제시하고 조직 내 의사결정 과정을 연구하여 노벨 경제학상을 수상한 미국의 경제학자, 인지심리학자, 컴퓨터 과학자이자 철학자이며, 인공지능 분야 초기 연구에 기여했고 카네기 멜론 대학교에서 교수로 재직하며 인지과학 발전에 영향을 미쳤다. - 카네기 멜런 대학교 교수 - 제프리 힌턴
제프리 힌턴은 심층 신경망 연구의 선구자로서, 역전파 알고리즘 개선 및 효과적인 학습 방법 개발에 기여하여 튜링상을 수상하고 볼츠만 머신 공동 발명, t-SNE 시각화 기법 개발 등 다양한 신경망 연구에 기여했으며, AI 위험성에 대한 우려를 표명하며 구글을 퇴사하고 존 호프필드와 함께 노벨 물리학상을 수상한 인지 심리학자이자 컴퓨터 과학자이다. - IEEE 석학회원 - 잭 킬비
잭 킬비는 미국의 전자 공학 기술자이자 집적 회로의 공동 발명가로, 1958년 단일 반도체 재료에 회로 부품을 집적하는 아이디어를 제시하고 1959년 최초의 집적 회로에 대한 특허를 출원했으며, 2000년 노벨 물리학상을 수상했다. - IEEE 석학회원 - 리카이푸
리카이푸는 음성 인식 기술 개발자이자 애플, 마이크로소프트, 구글 등 주요 기업을 거쳐 시노베이션 벤처스와 01.AI를 설립한 벤처 투자가이며, 인공지능 분야 저술 및 강연 활동도 활발히 하고 있다. - 미국에서 코로나19로 죽은 사람 - 콜린 파월
콜린 파월은 미국의 군인이자 정치인으로, 육군 대장까지 진급하여 국가안보보좌관, 합참의장, 국무장관을 역임했으며, 특히 최초의 아프리카계 미국인 합참의장 및 국무장관으로 알려져 있다. - 미국에서 코로나19로 죽은 사람 - 찰리 프라이드
미국의 컨트리 음악 가수이자 야구 선수였던 찰리 프라이드는 니그로 리그와 마이너 리그에서 야구 선수로 활동하다 1960년대 중반부터 컨트리 음악 가수로 성공하여 "Kiss an Angel Good Mornin'" 등의 히트곡을 내고 컨트리 음악 명예의 전당에 헌액되는 업적을 남겼다.
| 에드먼드 M. 클라크 - [인물]에 관한 문서 | |
|---|---|
| 기본 정보 | |
 | |
| 출생 이름 | Edmund Melson Clarke, Jr. |
| 출생일 | 1945년 7월 27일 |
| 출생지 | 미국 버지니아주 뉴포트뉴스 |
| 사망일 | 2020년 12월 22일 |
| 사망지 | 미국 펜실베이니아주 피츠버그 |
| 분야 | 컴퓨터 과학 |
| 직장 | 카네기 멜런 대학교 |
| 모교 | 코넬 대학교 |
| 학위 논문 제목 | Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems |
| 학위 논문 년도 | 1976년 |
| 박사 지도 학생 | |
| 알려진 업적 | 모델 검증 |
| 수상 | 튜링상 |
| 웹사이트 | 에드먼드 클라크 웹사이트 |
| 참고 사항 | |
| 수상 경력 | 튜링상 |
2. 생애
클라크는 버지니아주 뉴포트 뉴스에서 태어났다. 버지니아 대학교에서 1967년 수학 학사, 듀크 대학교에서 1968년 수학 석사, 코넬 대학교에서 1976년 컴퓨터 과학 박사 학위를 받았다. 박사 학위 취득 후 2년간 듀크 대학교 컴퓨터 과학과 교수로 재직했으며, 1978년 하버드 대학교 하버드 공학 및 응용 과학부 컴퓨터 과학 조교수가 되었다. 1982년 카네기 멜론 대학교 컴퓨터 과학과 교수로 합류, 1989년 정교수가 되었다. 1995년 카네기 멜론 컴퓨터 과학 대학 FORE 시스템즈 석좌 교수로 최초 임명되었고, 2008년 대학 교수, 2015년 명예 교수가 되었다.[2]
2020년 12월, 펜실베이니아주에서 코로나19 범유행 중 코로나19로 인해 75세의 나이로 사망했다.[3][4]
2. 1. 초기 생애 및 교육
클라크는 버지니아주 뉴포트 뉴스에서 태어나 1967년 버지니아 대학교 샬러츠빌에서 문학사 학위를, 1968년 듀크 대학교 노스캐롤라이나주 더럼에서 문학석사 학위를, 1976년 코넬 대학교 뉴욕주 이타카에서 컴퓨터 과학 철학박사 학위를 받았다.[2] 박사 학위를 받은 후 2년 동안 듀크 대학교 컴퓨터 과학과에서 가르쳤다. 1978년에는 매사추세츠주 캠브리지에 있는 하버드 대학교로 옮겨 하버드 공학 및 응용 과학부에서 컴퓨터 과학 조교수로 재직했다. 1982년 하버드를 떠나 펜실베이니아주 피츠버그에 있는 카네기 멜론 대학교 컴퓨터 과학과 교수로 합류했다. 1989년 정교수로 임명되었다. 1995년에는 카네기 멜론 컴퓨터 과학 대학의 기금 강좌인 FORE 시스템즈 석좌 교수로 최초로 임명되었다. 2008년에는 대학 교수가 되었고 2015년에는 명예 교수가 되었다.[2]2. 2. 학문 경력
클라크는 버지니아주 뉴포트 뉴스에서 태어났다. 1967년 버지니아 대학교에서 문학사 학위를, 1968년 듀크 대학교에서 문학석사 학위를, 1976년 코넬 대학교에서 컴퓨터 과학 철학박사 학위를 받았다. 박사 학위 취득 후 2년 동안 듀크 대학교 컴퓨터 과학과에서 교수로 재직했다. 1978년 하버드 대학교로 옮겨 하버드 공학 및 응용 과학부에서 컴퓨터 과학 조교수로 재직했다. 1982년 카네기 멜론 대학교 컴퓨터 과학과 교수로 합류했으며, 1989년 정교수가 되었다. 1995년 카네기 멜론 컴퓨터 과학 대학의 기금 강좌인 FORE 시스템즈 석좌 교수로 최초 임명되었다. 2008년 대학 교수가 되었고, 2015년 명예 교수가 되었다.[2]2. 3. 사망
2020년 12월, 펜실베이니아주에서 코로나19 범유행 중 코로나19로 인해 75세의 나이로 사망했다.[3][4] 같은 해 12월 22일, 아들 제임스의 트위터와 카네기 멜론 대학교를 통해 사망 소식이 발표되었다.[6]3. 연구 업적
클라크는 소프트웨어 및 하드웨어 검증과 자동 정리 증명 분야에 관심을 가졌다.[5] 그는 박사 학위 논문에서 특정 프로그래밍 언어 제어 구조가 좋은 호어 스타일 증명 시스템을 갖지 못한다는 것을 증명했다.[5] 그의 연구 그룹은 최초의 병렬 해결 자동 정리 증명기인 파르테논과 기호 계산 시스템을 기반으로 한 정리 증명기인 Analytica를 개발했다.[5]
3. 1. 모델 검증
1981년, E. 앨런 에머슨과 함께 유한 상태 병렬 시스템의 검증 기술로 모델 검증을 사용하는 것을 처음 제안했다.[5] 그의 연구 그룹은 하드웨어 검증에 모델 검증을 사용하는 것을 개척했다.[5] 이진 결정 다이어그램을 사용한 기호적 모델 검증 또한 그의 그룹에 의해 개발되었다.[5] 이 중요한 기술은 케네스 맥밀란이 박사 학위 논문의 주제로 삼았으며, ACM 박사 논문상을 받았다.[5]3. 2. 기호적 모델 검증
클라크는 소프트웨어 및 하드웨어 검증과 자동 정리 증명 분야에 관심을 가졌다. 1981년, 박사 과정 학생인 E. 앨런 에머슨과 함께 유한 상태 병렬 시스템의 검증 기술로 모델 검증을 처음 제안했다.[5] 그의 연구 그룹은 하드웨어 검증에 모델 검증을 사용하는 것을 개척했으며,이진 결정 다이어그램을 사용한 기호적 모델 검증 또한 그의 그룹에 의해 개발되었다.[5] 이 기술은 ACM 박사 논문상을 받은 케네스 맥밀란의 박사 학위 논문 주제였다.[5]3. 3. 자동 정리 증명기 개발
클라크의 관심 분야는 소프트웨어 및 하드웨어 검증과 자동 정리 증명이었다.[5] 그는 박사 학위 논문에서 특정 프로그래밍 언어 제어 구조가 좋은 호어 스타일 증명 시스템을 갖지 못한다는 것을 증명했다.[5] 1981년, 그는 박사 과정 학생인 E. 앨런 에머슨과 함께 모델 검증을 유한 상태 병렬 시스템의 검증 기술로 사용하는 것을 처음 제안했다.[5] 그의 연구 그룹은 하드웨어 검증에 모델 검증을 사용하는 것을 개척했다.[5] 이진 결정 다이어그램을 사용한 기호적 모델 검증 또한 그의 그룹에 의해 개발되었다.[5] 이 중요한 기술은 ACM 박사 논문상을 받은 케네스 맥밀란의 박사 학위 논문의 주제였다.[5] 또한, 그의 연구 그룹은 최초의 병렬 해결 자동 정리 증명기 (파르테논)와 기호 계산 시스템을 기반으로 한 정리 증명기 (Analytica)를 개발했다.[5]3. 4. 복잡계 계산 모델링 및 분석 센터
1981년, 클라크는 박사 과정 학생인 E. 앨런 에머슨과 함께 모델 검증을 유한 상태 병렬 시스템의 검증 기술로 사용하는 것을 처음 제안했다. 그의 연구 그룹은 하드웨어 검증에 모델 검증을 사용하는 것을 개척했다. 이진 결정 다이어그램을 사용한 기호적 모델 검증 또한 그의 그룹에 의해 개발되었다. 이 중요한 기술은 ACM 박사 논문상을 받은 케네스 맥밀란의 박사 학위 논문의 주제였다. 또한, 그의 연구 그룹은 최초의 병렬 해결 자동 정리 증명기 (파르테논)와 기호 계산 시스템을 기반으로 한 정리 증명기 (Analytica)를 개발했다.[5] 2009년, 그는 국립 과학 재단의 자금 지원을 받아 복잡계의 계산 모델링 및 분석 (CMACS) 센터를 설립하는 것을 주도했다. 이 센터는 여러 대학에 걸쳐 있는 연구팀을 보유하고 있으며, 추상 해석과 모델 검증을 생물학 및 임베디드 시스템에 적용하고 있다.4. 수상 및 영예
ACM과 IEEE의 회원이었다. 1995년 반도체 연구 공사로부터 기술 우수상을 받았고, 1999년 카네기 멜론 대학교 컴퓨터 과학과에서 앨런 뉴웰 연구 우수상을 받았다. 랜달 브라이언트, E. 앨런 에머슨, 케네스 맥밀란과 함께 1999년 기호적 모델 검증 개발에 기여한 공로로 ACM 파리 카넬라키스 상을 공동 수상했다. 2004년에는 하드웨어 및 소프트웨어 시스템의 형식적 검증에 대한 중요하고 선구적인 기여와 이러한 기여가 전자 산업에 미친 지대한 영향으로 IEEE 컴퓨터 협회 해리 H. 굿 기념상을 받았다. 그는 하드웨어 및 소프트웨어 정확성 형식적 검증에 기여한 공로로 2005년 미국 공학 한림원에 선출되었다. 2011년 미국 예술 과학 아카데미에 선출되었다. 그는 "모델 검증 발명에 기여하고 20년 이상 이 분야에서 지속적으로 리더십을 발휘한 공로"를 인정받아 2008년 에르브랑 상을 수상했다. 2012년에는 정보학 분야에 대한 탁월한 기여를 인정받아 빈 공과대학교에서 명예 박사 학위를 받았다. 그는 "운송, 통신, 의학 분야를 포함한 광범위한 컴퓨터 시스템의 정확성을 자동으로 검증하는 기술의 구상과 개발에 대한 선도적인 역할"로 인해 2014년 프랭클린 연구소로부터 바우어 과학 업적상을 받았다. 그는 시그마 시와 파이 베타 카파의 회원이었다. 2007년에는 어렌 에머슨, 조셉 시파키스와 함께 튜링상을 수상했다.[1]
참조
[1]
웹사이트
Edmund Melson Clarke, Jr.
https://www.laughlin[...]
[2]
웹사이트
Edmund M. Clarke
https://www.cs.cmu.e[...]
2020-12-24
[3]
트윗
My father, Edmund M Clarke, passed away from Covid today. [...]
2020-12-22
[4]
웹사이트
Edmund Clarke Pioneered Methods For Detecting Software, Hardware Errors | Carnegie Mellon School of Computer Science
https://www.cs.cmu.e[...]
2020-12-24
[5]
간행물
Analytica – An Experiment in Combining Theorem Proving and Symbolic Computation
1998
[6]
뉴스
Edmund Clarke Pioneered Methods For Detecting Software, Hardware Errors
https://www.cmu.edu/[...]
2020-12-25
[7]
트윗
My father, Edmund M Clarke, passed away from Covid today. [...]
2020-12-22
[8]
웹인용
Edmund Clarke Pioneered Methods For Detecting Software, Hardware Errors | Carnegie Mellon School of Computer Science
https://www.cs.cmu.e[...]
2020-12-24
본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.
문의하기 : help@durumis.com