관리자
50
2024-05-21
내역사업 | 우수신진연구 |
---|
과제명 | 멀티코어 소프트웨어 검증 이론 개발 및 실제 시스템에 적용 | ||||
---|---|---|---|---|---|
과제고유번호 | 1711111853 | ||||
부처명 | 과학기술정보통신부 | ||||
시행계획 내 사업명 | |||||
시행계획 내 사업유형 | 예산출처지역 | 대전광역시 | 사업수행지역 | 대전광역시 | |
계속/신규 과제구분 | 신규과제 | ||||
과제수행연도 | 2020 | 총연구기간 | 2020-03-01 ~ 2023-02-28 | 당해연도 연구기간 | 2020-03-01 ~ 2021-02-28 |
연구목표 | **효율적인 멀티코어 소프트웨어를 수학적인 명세부터 실행가능한 머신 코드까지 엄밀하게 검증하기 위한 이론을 개발하고 실제 시스템에 적용***목표 1: 이론 개발.* 효율적인 논블로킹 (nonblocking) 멀티코어 소프트웨어를 엄밀하게 검증하기 위한 최첨단 이론인 동시성 분리 논리는 (concurrent separation logic) 아직 실제 멀티코어... | ||
---|---|---|---|
연구내용 | *이론 개발 1: 동시성 분리 논리에서 SC fence 지원*. 기존 동시성 분리 논리를 확장하여 SC fence를 사용해 동기화한 프로그램을 검증할 수 있도록 지원한다. 이를 통해 실제 멀티코어 시스템에서 사용되는 느슨한 동시성을 위한 동기화 기법을 검증할 수 있게 된다.*이론 개발 2: 논블로킹 멀티코어 프로그램을 위한 컴파일러 검증.* 소스 코드만이 ... | ||
기대효과 | **멀티코어 프로그램의 안전성, 정확성과 효율성 확보***안전성과 정확성.* 멀티코어 프로그램은 본질적인 비결정성으로 인해 안전성과 정확성을 확신하기 매우 어렵다. 코드 리뷰나 테스팅도 싱글코어 프로그램과는 달리 멀티코어 프로그램에서는 효과적이지 않다. 따라서 멀티코어 프로그램의 안전성과 정확성을 확신하기 위해서는 반드시 엄밀하게 검증해야 한다. 이 연구과... | ||
키워드 | 멀티코어,동시성,프로그램 검증,분리 논리,컴파일러 검증,시뮬레이션 |
단독연구 | 기업 | 대학 | 국공립(연)/출연(연) | 외국연구기관 | 기타 |
---|---|---|---|---|---|
|
연구개발단계 | 기초연구 | 산업기술분류 | |
---|---|---|---|
미래유망신기술(6T) | IT(정보기술) | 기술수명주기 | |
연구수행주체 | 학 | 과학기술표준분류 | 인공물 > 정보/통신 > 정보이론 > 프로그래밍 언어/자연어 처리 |
주력산업분류 | 적용분야 | 지식의 진보(비목적연구) | |
중점과학기술분류 | 과제유형 |
과제수행기관(업) 정보 | 과제수행기관(업)명 | 한국과학기술원 | 사업자등록번호 | |
---|---|---|---|---|
연구책임자 | 소속기관명 | 한국과학기술원 | 사업자등록번호 | |
최종학위 | 박사 | 최종학력전공 | 공학 |
국비 | 211,000,000 | 지방비(현금+현물) | 0 |
---|---|---|---|
비고 |