이광근 프로그램분석 시스템 연구단 ropas.kaist.ac.kr KAIST 전산학과

Slides:



Advertisements
Similar presentations
소프트웨어 및 로봇 활용 교육 부제 : 소프트웨어를 부탁해 포스코 포항 창조경제센터. 교육 상세일정 일자시간소요시간내용담당교사교육공간교보재 8/17( 월 ),8/19( 수 ) 12:50 ~ 13:10 20 분접수 및 수업준비유레카 카페 13:10 ~ 13:20 10 분프로그램.
Advertisements

Cinema Manager System 최종 발표 조 team05 발표자 : 임 창목 1.
2014 하반기 대졸 신입 / 인턴 / 장학생 모집 모집 분야분류세부직무신입인턴장학생관련전공 R&D 설계 전기, 전자, 전파, 반도체, 정보통신, 컴퓨터, 물리 CAE 전기, 전자, 전파, 반도체, 정보통신, 컴퓨터, 물리 소자 반도체,
지도교사 : 김은이 선생님 연현초등학교 5 학년 조인해 연현초등학교 5 학년 최지원 우리는 항상 먹기 싫은 쓴 약을 먹을 때 달콤한 주스 나 탄산음료와 함께 마시면 쓴 약을 쉽게 먹을 수 있 을 텐데, 사람들은 감기약, 두통약, 영양제등과 같은 알약을 먹을 때 너무나.
창의적 교육과정: 실적 현황 2013년 및 2014년 신규 교과목 14개 개발, 개설
2012년도 1학기 인하대학교 IT공과대학 전자공학부/정보통신학부 공동 세미나 (협찬: 차세대 DTV 인력양성사업)
(4) 우리 나라의 이상과 목표 2. 국가의 중요성과 국가 발전 중학교 2학년 도덕
1. 과학중점학교 어떤 학교인가? 1. 과학중점학교 어떤 학교인가? 일반 인문계고등학교에서 인문학적 소양과 더불어
HTC Polisher 인벤터 사랑 디자인 컨테스트 작품명: HTC 2500ix 1.
Secure Coding 이학성.
팀명 : 정효가현팀 팀원 : 김효진, 이가현, 이정민
비뇨계통.
2014 하반기 대졸 신입/인턴/장학생 모집 모집 분야 분류 세부직무 신입 인턴 장학생
1. 근접경호의 개념 경호대상의 신변을 보호하기 위하여 지근거리에서 실시하는 호위활동을 말하며 경호행위의 마지막 보루이다.
메탄 하이드레이트 활용 방법과 기술 환경공학과 천대길.
로봇 소프트웨어.
이광근 교수 Programming Research Laboratory ropas.snu.ac.kr
1-1 일과 일률.
시스템집적반도체 설계 검증 환경과 기법 Ch 7.
최현진 정경대학 정치외교학과 국제정치론 2014 가을학기 제1주(2) 최현진 정경대학 정치외교학과
한국 에이브이엘 ㈜ (AVL Korea)
Capstone-Design : IoTeam Introduction Abstract
시스템 설계와 산업디자인 개발.
컴퓨터과학 전공탐색 배상원.
현장실습(Co-Operation) 소감 발표
1. 현대 생활과 응용 윤리의 필요성 2. 윤리 문제의 탐구와 실천 3. 윤리 문제에 대한 다양한 접근
Smart Sensing Window 인제대학교 컴퓨터시뮬레이션학과 이동규.
건축설계사 임동진.
Computational Thinking
소프트웨어 오류 자동 검증 기술.
학과 : E-BIZ 경영학과 학번 : 이름 : 홍 지 애
교육과정과 주요업무.
(신)비취가인천비방진연3종기획1 182,000 ▶ 91,000 (신)비취가인 천비방 진연수
소규모 IPTV 사업자용 실시간 미디어 플랫폼 기술
LIT-GenAppSetup ※ Texting+ 클라이언트 프로그램은 제품 인증을 받은 제품입니다.
기능안전 설계 지원 프로세서 코어(알데바란) 06
남다른 아이로 미래를 디자인하라!.
HEVC기반 실시간 Full-HD 비디오 플레이어 기술)
소금물과 물의 부력 차이 실험 작성자 - 백민준.
AUTODESK AUTOCAD ELECTRICAL 전기제어 2D 설계 소프트웨어 표준기반 설계 생산성 도구 구조도 설계
사과는 왜 갈변 할까? 조장: 31017유수빈 조원:31024이지은.
프로그램 분석 기술의 산업체 이전을 위해서 이광근 서울대 컴퓨터공학부
메모리 타입 분석을 통한 안전하고 효율적인 메모리 재사용
청정 에너지 프로젝트 분석 소개 청정에너지 프로젝트 분석 과정
7주차 실습 FPGA 보드 사용법.
메카트로닉스공학과 메카트로닉스공학과란? 홈페이지 │
영상인식분야 개발계획서 ○ ○ 대학교 팀명 제13회 현대자동차그룹 미래자동차 기술공모전
Cold Spring Harbor Laboratory Press 저널 이용 매뉴얼
과학 1 학년 2 학기 생명> 04.태아의 발생 과정은 어떻게 진행될까?[ 4 / 6 ] 수정과 착상 수업계획 수업활동.
<2013 과학탐구 보고서> 우유와 발효유가 일정온도에서 만나면?
㈜엔프라넷.
프로그램분석 어떻게하나 (quick/tiny)
인공 지능 시대에 필요한 인재 행복한 미래를 만드는 기술자 김송호.
(Wed) Hyun Woong Nam.
웹 사이트 분석과 설계 [디자인 리서치] 학번: 이름 : 홍지애.
P 보일의 법칙 - 생각열기 – 기포가 수면으로 올라가면 크기는 어떻게 될까?
Ⅱ. 물질의 특성 물질의 끓는점.
외국인 노동자 고용사례 일어일문 정 솔.
1학년 신입생 학부모교실 안내사항 2019년 3월 6일 1학년부장 김희선.
자료구조 강의소개 정성훈 연락처 : 이메일 : 연구실 : 연219호 연락처 : 이메일 : 홈페이지: 정성훈.
.Net FrameWork for Web2.0 한석수
1장 C 언어의 개요 C 언어의 역사와 기원 C 언어의 특징 프로그램 과정 C 프로그램 구조 C 프로그램 예제.
교량 구조물의 개념 설계 및 프로토타입 제작 과정
1. 강의 소개 컴퓨팅적 사고와 문제해결.
(Motion fusion based static and dynamic hand gesture recognition)
SNU 컴퓨터의 기초 월 14:00-16:00 43동101호 ropas. snu. ac
펌웨어(S/W) Upgrade 방법 Samsung Kies3
AUTOSAR 기반 차량 전장용 운영체제 및 MCAL 기술 V2.0
7 생성자 함수.
1 제조 기술의 세계 3 제품의 개발과 표준화 제품의 개발 표준화 금성출판사.
Presentation transcript:

이광근 프로그램분석 시스템 연구단 ropas.kaist.ac.kr KAIST 전산학과 소프트웨어 분석기술의 산업체 적용 이광근 프로그램분석 시스템 연구단 ropas.kaist.ac.kr KAIST 전산학과 3/29/2002 만도기계 중앙연구소

프로그램 분석 시스템 연구단 1998년 9월 과학기술부 창의적연구진흥사업 지정 연구센터 목표: 안전한 프로그램의 생성 기술 핵심: 프로그램 분석(static analysis) 1단계(1998-2001): 연구위주 2단계(2002-2005): 산업체와의 협력 3/29/2002 만도중앙연구소 KAIST 프로그램분석시스템 연구단

프로그램 분석기술 프로그램이 실행중에 어떤 일을 하는 지를 미리 확인하는 자동화된 기술 “미리”? “확인”? “자동화”? 소프트웨어를 제품에 심어서 출시하기전에 제품의 품질과 직결 “확인”? 엄밀한 방법: 안심 (모든경우 O) 테스트/시뮬레이션: 불안 (모든경우 X) “자동화”? 프로그램을 분석해 주는 소프트웨어 3/29/2002 만도중앙연구소 KAIST 프로그램분석시스템 연구단

프로그램 분석기술 적용예 실행중에 처리되지 않는 예외상황이 있는가? 실행중에 메시지 큐가 overflow없이 작동하는가? Java, ML 프로그램 분석 (~300lines/sec) 실질적으로 ML컴파일러에 장착됨 실행중에 메시지 큐가 overflow없이 작동하는가? KAIST 과학위성에 내장될 소프트웨어 모듈 concurrent system (6 CPUs) 3/29/2002 만도중앙연구소 KAIST 프로그램분석시스템 연구단

연구단의 기술 프로그램 분석의 디자인 기술 디자인된 분석기의 엄밀한 검증 기술 디자인된 분석기의 자동 생성 기술 abstract interpretation, type inference, constraint-based analysis 디자인된 분석기의 엄밀한 검증 기술 mathematical proof 디자인된 분석기의 자동 생성 기술 System Z1, System Zoo 생성된 분석기를 이용한 대상 S/W 분석 분석결과의 해석 3/29/2002 만도중앙연구소 KAIST 프로그램분석시스템 연구단

산업체에 관심을 가지는 이유 (a) 전세계적으로 static analysis 기술이 학계에서 산업계로 이전되는 단계: GM, Daimler Chrysler, AirBus, Dassault, (Bosch) 등등 소프트웨어 품질 = 제품의 품질 우리 산업계에는? 자동차 부품 산업? 만도/현대/… 3/29/2002 만도중앙연구소 KAIST 프로그램분석시스템 연구단

산업체에 관심을 가지는 이유 (b) 연구된 기술: 학교,학계 (internationally recognized) 실제세계, 주변의 문제를 푸는데 어느정도 공헌할 수 있는지 국제적인 수준에서 외국동료들의 움직임 우리도 우리산업체와 함께 연구된(할) 기술을 갈고닦자 3/29/2002 만도중앙연구소 KAIST 프로그램분석시스템 연구단

방문협의 만도㈜의 자동차 핵심부품에 장착되는 S/W의 품질을 검증하는 데 우리의 기술이 적용될 여지는? 우리가 연구하는 기술이 실용적이기 위해서 놓치고 있는것은? “세계적인 산업체를 일구는 데 도움될 수 있기를” 3/29/2002 만도중앙연구소 KAIST 프로그램분석시스템 연구단