에드먼드 M. 클라크

1. 개요

에드먼드 M. 클라크는 소프트웨어 및 하드웨어 검증과 자동 정리 증명 분야에 기여한 컴퓨터 과학자이다. 버지니아 대학교에서 학사, 듀크 대학교에서 석사 학위를 받았으며 코넬 대학교에서 컴퓨터 과학 박사 학위를 취득했다. 듀크 대학교, 하버드 대학교, 카네기 멜론 대학교에서 교수로 재직했으며, 2007년 튜링상을 수상했다. 클라크는 모델 검증 기술을 개발하고, 기호적 모델 검증, 자동 정리 증명기 개발에 기여했으며, 2020년 코로나19로 사망했다.

2. 생애

클라크는 버지니아주 뉴포트 뉴스에서 태어났다. 버지니아 대학교에서 1967년 수학 학사, 듀크 대학교에서 1968년 수학 석사, 코넬 대학교에서 1976년 컴퓨터 과학 박사 학위를 받았다. 박사 학위 취득 후 2년간 듀크 대학교 컴퓨터 과학과 교수로 재직했으며, 1978년 하버드 대학교 하버드 공학 및 응용 과학부 컴퓨터 과학 조교수가 되었다. 1982년 카네기 멜론 대학교 컴퓨터 과학과 교수로 합류, 1989년 정교수가 되었다. 1995년 카네기 멜론 컴퓨터 과학 대학 FORE 시스템즈 석좌 교수로 최초 임명되었고, 2008년 대학 교수, 2015년 명예 교수가 되었다.

2020년 12월, 펜실베이니아주에서 코로나19 범유행 중 코로나19로 인해 75세의 나이로 사망했다.

2.1. 초기 생애 및 교육

클라크는 버지니아주 뉴포트 뉴스에서 태어나 1967년 버지니아 대학교 샬러츠빌에서 문학사 학위를, 1968년 듀크 대학교 노스캐롤라이나주 더럼에서 문학석사 학위를, 1976년 코넬 대학교 뉴욕주 이타카에서 컴퓨터 과학 철학박사 학위를 받았다. 박사 학위를 받은 후 2년 동안 듀크 대학교 컴퓨터 과학과에서 가르쳤다. 1978년에는 매사추세츠주 캠브리지에 있는 하버드 대학교로 옮겨 하버드 공학 및 응용 과학부에서 컴퓨터 과학 조교수로 재직했다. 1982년 하버드를 떠나 펜실베이니아주 피츠버그에 있는 카네기 멜론 대학교 컴퓨터 과학과 교수로 합류했다. 1989년 정교수로 임명되었다. 1995년에는 카네기 멜론 컴퓨터 과학 대학의 기금 강좌인 FORE 시스템즈 석좌 교수로 최초로 임명되었다. 2008년에는 대학 교수가 되었고 2015년에는 명예 교수가 되었다.

2.2. 학문 경력

클라크는 버지니아주 뉴포트 뉴스에서 태어났다. 1967년 버지니아 대학교에서 문학사 학위를, 1968년 듀크 대학교에서 문학석사 학위를, 1976년 코넬 대학교에서 컴퓨터 과학 철학박사 학위를 받았다. 박사 학위 취득 후 2년 동안 듀크 대학교 컴퓨터 과학과에서 교수로 재직했다. 1978년 하버드 대학교로 옮겨 하버드 공학 및 응용 과학부에서 컴퓨터 과학 조교수로 재직했다. 1982년 카네기 멜론 대학교 컴퓨터 과학과 교수로 합류했으며, 1989년 정교수가 되었다. 1995년 카네기 멜론 컴퓨터 과학 대학의 기금 강좌인 FORE 시스템즈 석좌 교수로 최초 임명되었다. 2008년 대학 교수가 되었고, 2015년 명예 교수가 되었다.

2.3. 사망

2020년 12월, 펜실베이니아주에서 코로나19 범유행 중 코로나19로 인해 75세의 나이로 사망했다. 같은 해 12월 22일, 아들 제임스의 트위터와 카네기 멜론 대학교를 통해 사망 소식이 발표되었다.

3. 연구 업적

클라크는 소프트웨어 및 하드웨어 검증과 자동 정리 증명 분야에 관심을 가졌다. 그는 박사 학위 논문에서 특정 프로그래밍 언어 제어 구조가 좋은 호어 스타일 증명 시스템을 갖지 못한다는 것을 증명했다. 그의 연구 그룹은 최초의 병렬 해결 자동 정리 증명기인 파르테논과 기호 계산 시스템을 기반으로 한 정리 증명기인 Analytica를 개발했다.

3.1. 모델 검증

1981년, E. 앨런 에머슨과 함께 유한 상태 병렬 시스템의 검증 기술로 모델 검증을 사용하는 것을 처음 제안했다. 그의 연구 그룹은 하드웨어 검증에 모델 검증을 사용하는 것을 개척했다. 이진 결정 다이어그램을 사용한 기호적 모델 검증 또한 그의 그룹에 의해 개발되었다. 이 중요한 기술은 케네스 맥밀란이 박사 학위 논문의 주제로 삼았으며, ACM 박사 논문상을 받았다.

3.2. 기호적 모델 검증

클라크는 소프트웨어 및 하드웨어 검증과 자동 정리 증명 분야에 관심을 가졌다. 1981년, 박사 과정 학생인 E. 앨런 에머슨과 함께 유한 상태 병렬 시스템의 검증 기술로 모델 검증을 처음 제안했다. 그의 연구 그룹은 하드웨어 검증에 모델 검증을 사용하는 것을 개척했으며,이진 결정 다이어그램을 사용한 기호적 모델 검증 또한 그의 그룹에 의해 개발되었다. 이 기술은 ACM 박사 논문상을 받은 케네스 맥밀란의 박사 학위 논문 주제였다.

3.3. 자동 정리 증명기 개발

클라크의 관심 분야는 소프트웨어 및 하드웨어 검증과 자동 정리 증명이었다. 그는 박사 학위 논문에서 특정 프로그래밍 언어 제어 구조가 좋은 호어 스타일 증명 시스템을 갖지 못한다는 것을 증명했다. 1981년, 그는 박사 과정 학생인 E. 앨런 에머슨과 함께 모델 검증을 유한 상태 병렬 시스템의 검증 기술로 사용하는 것을 처음 제안했다. 그의 연구 그룹은 하드웨어 검증에 모델 검증을 사용하는 것을 개척했다. 이진 결정 다이어그램을 사용한 기호적 모델 검증 또한 그의 그룹에 의해 개발되었다. 이 중요한 기술은 ACM 박사 논문상을 받은 케네스 맥밀란의 박사 학위 논문의 주제였다. 또한, 그의 연구 그룹은 최초의 병렬 해결 자동 정리 증명기 (파르테논)와 기호 계산 시스템을 기반으로 한 정리 증명기 (Analytica)를 개발했다.

3.4. 복잡계 계산 모델링 및 분석 센터

1981년, 클라크는 박사 과정 학생인 E. 앨런 에머슨과 함께 모델 검증을 유한 상태 병렬 시스템의 검증 기술로 사용하는 것을 처음 제안했다. 그의 연구 그룹은 하드웨어 검증에 모델 검증을 사용하는 것을 개척했다. 이진 결정 다이어그램을 사용한 기호적 모델 검증 또한 그의 그룹에 의해 개발되었다. 이 중요한 기술은 ACM 박사 논문상을 받은 케네스 맥밀란의 박사 학위 논문의 주제였다. 또한, 그의 연구 그룹은 최초의 병렬 해결 자동 정리 증명기 (파르테논)와 기호 계산 시스템을 기반으로 한 정리 증명기 (Analytica)를 개발했다. 2009년, 그는 국립 과학 재단의 자금 지원을 받아 복잡계의 계산 모델링 및 분석 (CMACS) 센터를 설립하는 것을 주도했다. 이 센터는 여러 대학에 걸쳐 있는 연구팀을 보유하고 있으며, 추상 해석과 모델 검증을 생물학 및 임베디드 시스템에 적용하고 있다.

4. 수상 및 영예

ACM과 IEEE의 회원이었다. 1995년 반도체 연구 공사로부터 기술 우수상을 받았고, 1999년 카네기 멜론 대학교 컴퓨터 과학과에서 앨런 뉴웰 연구 우수상을 받았다. 랜달 브라이언트, E. 앨런 에머슨, 케네스 맥밀란과 함께 1999년 기호적 모델 검증 개발에 기여한 공로로 ACM 파리 카넬라키스 상을 공동 수상했다. 2004년에는 하드웨어 및 소프트웨어 시스템의 형식적 검증에 대한 중요하고 선구적인 기여와 이러한 기여가 전자 산업에 미친 지대한 영향으로 IEEE 컴퓨터 협회 해리 H. 굿 기념상을 받았다. 그는 하드웨어 및 소프트웨어 정확성 형식적 검증에 기여한 공로로 2005년 미국 공학 한림원에 선출되었다. 2011년 미국 예술 과학 아카데미에 선출되었다. 그는 "모델 검증 발명에 기여하고 20년 이상 이 분야에서 지속적으로 리더십을 발휘한 공로"를 인정받아 2008년 에르브랑 상을 수상했다. 2012년에는 정보학 분야에 대한 탁월한 기여를 인정받아 빈 공과대학교에서 명예 박사 학위를 받았다. 그는 "운송, 통신, 의학 분야를 포함한 광범위한 컴퓨터 시스템의 정확성을 자동으로 검증하는 기술의 구상과 개발에 대한 선도적인 역할"로 인해 2014년 프랭클린 연구소로부터 바우어 과학 업적상을 받았다. 그는 시그마 시와 파이 베타 카파의 회원이었다. 2007년에는 어렌 에머슨, 조셉 시파키스와 함께 튜링상을 수상했다.