1954년 6월 2일, 미국의 컴퓨터과학자 E. 앨런 에머슨 (E. Allen Emerson, 1954 ~ 2024) 출생

1954년 6월 2일, 미국의 컴퓨터과학자 E. 앨런 에머슨 (E. Allen Emerson, 1954 ~ 2024) 출생

E. 앨런 에머슨 (E. Allen Emerson, 1954년 6월 2일 ~ 2024년 10월 15일)은 미국의 컴퓨터 과학자이자 2007년 튜링상 수상자이다.

– E. 앨런 에머슨 (E. Allen Emerson)

.본명: 어니스트 앨런 에머슨 2세 (Ernest Allen Emerson II)

.출생: 1954년 6월 2일

.사망: 2024년 10월 15일 (71세)

.성별: 남성

.국적: 미국

.경력: 텍사스 대학교 오스틴 교수, 리전트 의장

.직업: 컴퓨터 과학자

.학력: 텍사스 대학교 오스틴 (응용수학 / 1976년 학사), 하버드 대학교 (응용수학 / 1981년 박사)

.지도 교수: 에드먼드 클라크 (Edmund Melson Clarke Jr.)

.소속: 텍사스 대학교 오스틴 (컴퓨터 과학 / 교수)

.상훈: 2007년 튜링상

– 생애 및 활동

E. 앨런 에머슨은 1954년 6월 2일에 출생했다.

본명은 어니스트 앨런 에머슨 2세 (Ernest Allen Emerson II)다.

텍사스 대학교 오스틴 (응용수학 / 1976년 학사), 하버드 대학교 (응용수학 / 1981년 박사)에서 학업했다.

1980년대 초, 에머슨과 그의 박사 학위 지도교수인 에드먼드 M. 클라크는 유한 상태 시스템을 형식적 명세 에 대해 검증하는 기법을 개발했다.

그들은 이 개념에 대해 모델 검사라는 용어를 만들었고 , 이는 유럽에서 조셉 시파키스가 독립적으로 연구했다.

이러한 모델이라는 단어의 의미는 수리 논리학에서 모델 이론의 용법과 일치한다 . 즉, 시스템을 명세의 모델이라고 한다.

모델 검사에 관한 에머슨의 작업에는 사양을 설명하기 위한 초기의 영향력 있는 시간 논리와 상태 공간 폭발을 줄이기 위한 기술이 포함되었다.

에머슨은 텍사스 대학교 오스틴의 교수이자 리전트 (Regents) 의장을 역임했다.

에머슨은 소프트웨어 및 하드웨어의 공식 검증에 사용되는 기술인 모델 검사의 발명 및 개발에 대해 에드먼드 M. 클라크 및 조셉 시파키스와 함께 인정을 받았다.

시간 논리 및 모달 논리에 대한 그의 기여에는 동시 시스템 검증에 사용되는 계산 트리 논리 (CTL) 및 확장 CTL의 도입이 포함된다.

또한 많은 모델 검사 알고리즘에서 발생하는 조합 폭발을 해결하기 위해 상징적 모델 검사를 개발한 공로로 다른 사람들과 함께 인정받고 있다.

E. 앨런 에머슨은 2024년 10월 15일에 별세했다. 향년 71세

– 주요 업적

.모델 검사 개발: 에드먼드 M. 클라크 (Edmund M. Clarke) 및 그의 박사 과정 학생이었던 조셉 시파키스 (Joseph Sifakis)와 함께 모델 검사의 개념을 개척했다. 모델 검사는 하드웨어 및 소프트웨어 시스템의 정확성을 자동으로 검증하는 기술이다.

.전산 논리 분야 기여: 전산 논리 (Computational Logic), 특히 시제 논리 (Temporal Logic)를 사용하여 시스템의 동작을 기술하고 검증하는 방법에 대한 연구를 수행했다.

– 수상

2007년에 에머슨, 클라크, 시파키스는 튜링상을 수상했다.

하드웨어 및 소프트웨어 산업에서 널리 채택된 매우 효과적인 검증 기술로 모델 검사를 개발하는 데 기여한 공로를 인정받았다.

튜링상 외에도 에머슨은 랜달 브라이언트, 클라크, 케네스 L. 맥밀런과 함께 상징적 모델 검사 개발에 대한 공로로 1998년 ACM 파리 카넬라키스상을 수상했다.

컴퓨터 하드웨어 산업에서 널리 사용되고 있으며 소프트웨어 검증 및 기타 분야에서도 상당한 가능성을 보여주기 시작한 시스템 설계를 공식적으로 검사하는 방법인 상징적 모델 검사를 발명한 공로를 인정받았다.

참고 = 위키백과

리스천라이프 편집부