4541.664A Program Analysis: Theories and Practices

이광근 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" 등.

이 강좌에서는 정적 프로그램 분석 기술들의 이론과 실제를 익힌다. 이 목표를 위해서 두 부분으로 구성된다.

• 강의중심 Lecture-based Teaching:
  위의 모든 기술들을 아우를 수 있는 가장 강력한 틀인 요약해석(abstract interpretation)의 이론과 실제를 강의와 숙제를 통해서 익힌다.
• 문제중심 Problem-based Teaching:
  각 팀의 프로젝트 과제를 중심으로 프로그램 분석 이론을 실제 응용에 적용하면서 속내용을 구체적으로 익힌다.

내용 Contents

• Preliminaries: abstract syntax, semantics, inductive definitions, logics and inference, fixpoints
• Semantic formalisms: natural semantics, structural operational semantics, abstract machine semantics, denotational semantics
• Abstract interpretation: abstraction, concretization, galois connection, correctness, fixpoint algorithms

• Type-based analysis: monomorphic type system, polymorphic type system, effect system, unification
• Constraint-based analysis: set constraints, flow logics, constraint solving
• Software model checking: model checking, program logics, abstraction refinement

규정 Policy

• 성적은 절대평가.
• 출석 100%는 필수. 어쩔 수 없는 경우는 반드시 사전 허락을 받는다.

읽을 논문 Papers

숙제및 시험 Homeworks & Exams

• 프로그래밍 숙제는 컴퓨터를 통해 제출합니다.
• 제출기한을 지나 48시간 이내로 늦어지면 10% 감점. 그 이후의 숙제는 받지 않습니다.
• 프로그램 숙제는 OCaml로 작성합니다.
• 왜 ML로 실습하는가?
• 숙제 시간표 (tentative)
  • HW1: due 3/17
  • HW2: due 3/24
  • HW3: due 3/31
  • HW4: due 4/07
  • HW5: due 4/14
  • HW6: due 4/21
  • Exam I: 5/04
  • HW7: due 4/28 5/14
  • HW8: due 5/05 5/21
• HW1: OCaml exercise. Due 3/17 24:00
• HW2: OCaml exercise, induction, fixpoint. 3/24 24:00
• HW3: fixpoint induction, fixpoint computation. 4/1 24:00
• HW4: instrumented interpreters. 4/8 24:00
• HW5: semantic equation extractor. 4/14 24:00
• HW6: semantic equation solver (ad-hoc). 4/23 24:00
• HW7: abstract domain functor implementation. 5/14 24:00 , hw7-functors.ml , hw7-example.ml

• Old exams
  • 2008: quiz 1, exam 1, final
  • 2007: take-home exam
  • 2006: final exam
  • 2005: exam1 (problem7-solution), exam2

진도및 자료 Slides & Resources

wk 1	preliminaries	book5-24, slide1
wk 2	semantic formalisms I	book25-50, slide2 , slide3
wk 3	semantic formalisms II	slide4 , slide5
wk 4	abstract interpretation I	book61-75, slide6, slide7
wk 5	abstract interpretation II	slide8, slide9
wk 6	abstract interpretation III	book74-108, slide10-1, slide10-2
wk 7	abstract interpretation IV	slide11 , slide12
wk 8	abstract interpretation V
wk 9	problem-based approach I
wk 10	problem-based approach II
wk 11	problem-based approach III
wk 12	problem-based approach IV

• To view/print PS(Postscript) files: Ghostview
• To view/print PDF files: Acrobat Reader