SNU 4541.664A Program Analysis: Theories and Practices
Lecture Movies (Spring 2013)
교수: 이광근 Kwangkeun Yi
소프트웨어무결점 연구센터/
프로그래밍 연구실/CSE/Seoul National University
목표 Objectives
제대로 작동할 지를 미리 검증할 수 없는 기계설계는 없다. 제대로 서있을 지를 미리 검증할 수 없는 건축설계는 없다. 인공물들이 자연세계에서 문제 없이 작동할 지를 미리 엄밀하게 분석하는 수학적 기술들은 잘 발달해 왔다. 뉴튼 역학, 미적분 방정식, 통계 역학등이 그러한 기술들일 것이다.
소프트웨어에 대해서는 어떤가? 작성한 소프트웨어가 제대로 실행될 지를 미리 엄밀하게 확인해 주는 기술들은 있는가? 이에 대한 답이 프로그램 분석(static program analysis)기술 이라는 이름으로 모여지는 기술들이다. 그동안 다양한 이름으로 다양한 수준에서 다양한 필요에 맞추어 불리워지는 기술들을 모두 포섭한다: "static analysis", "abstract interpretation", "type system", "software model checking", "data-flow analysis", "program logics and proof system" 등.
이 강좌에서는 정적 프로그램 분석 기술들의 이론과 실제를 익힌다.
(동영상 목차에서 섹션 n.m 에 해당하는 강의동영상은 n-m.mp4 입니다. 단, n이나 m이 한 자리인 경우 0n-0m.mp4입니다.)- 의미공간(semantic domains)
- 궁극을 드러내는 의미구조(denotational semantics)
- 프로그램의 실행 의미 예제(formal semantics examples)
- 프로그램 분석 개관(overview of program analysis)
- 요약해석(abstract interpretation overview)
- 요약해석 틀(abstract interpretation framework)
- 갈로아 연결과 고정점 정리(Galois connection, fixpoint theorem)
- 의미공간의 요약(abstraction of semantic domains)
- 기타(miscellanea)
- 의미구조 요약(abstraction of semantics)
- 명령형 언어에 대한 요약해석 디자인과 구현(abstract interpretation for imperative language)
- 넓히기와 좁히기(widening and narrowing)
- 계산 실행과정의 요약(abstraction of semantic functions)
- 해석방정식의 해로 분석하기(program analysis by equation solving)
- 타입 시스템(static type system)
- 타입 스타일의 프로그램 분석(type-based program analysis)
| Course Homepage |
| Lecture Slides |
| Homeworks & Exams |
| Papers |
| Web Board |
|
|
|
|
|
If you see this, then your browser is too broken to display this site properly. Please consider getting a browser upgrade. |