4541.664A Program Analysis: Theories and Practices

이광근 Kwangkeun Yi
Programming Research Lab./CSE/Seoul National University

목표 Objectives

제대로 작동할 지를 미리 검증할 수 없는 기계설계는 없다. 제대로 서있을 지를 미리 검증할 수 없는 건축설계는 없다. 인공물들이 자연세계에서 문제 없이 작동할 지를 미리 엄밀하게 분석하는 수학적 기술들은 잘 발달해 왔다. 뉴튼 역학, 미적분 방정식, 통계 역학등이 그러한 기술들일 것이다.

소프트웨어에 대해서는 어떤가? 작성한 소프트웨어가 제대로 실행될 지를 미리 엄밀하게 확인해 주는 기술들은 있는가? 이에 대한 답이 프로그램 분석(static program analysis)기술 이라는 이름으로 모여지는 기술들이다.

이 강의에서는 그러한 프로그램 분석 기술들의 이론과 실제를 익힌다.

내용 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%는 필수. 어쩔 수 없는 경우는 반드시 사전 허락을 받는다.

진도및 자료 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 , slide10 , slide10-1
wk 6	abstract interpretation III	book74-108, slide10-2 , slide11 , slide12
wk 7	type-based analysis I	slide14, slide15
wk 8	type-based analysis II	slide16, slide17
wk 9	type-based analysis III	slide18
wk 10	constraint-based analysis I	slide19, slide20
wk 11	constraint-based analysis II	slide21
wk 12	software model-checking I	slide22
wk 13	project presentation
	EXAM I	exam1(old), exam1(old)-answer7
	EXAM II	final exam, exam2(old)

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

읽을 논문 Papers

숙제 Homeworks

• HW1: reading, proof, Airac5 (due 3/16 13:00)
• HW2: semantics definition for C-- (due 4/06 13:00)
• HW3: Galois connection, abstract interpreter proof (due 5/02 13:00)
• HW4: collecting interpreter for C-- (due 5/06 24:00)
• Exam1: take-home exam 1 (due 5/09 13:00)
• HW5: paper reading (due 5/16 13:00)
• HW6: abstract interpreter for C-- (due 5/30 13:00, 24:00)
• Project candidates: interval analysis for C-- with dynamic malloc, effect inference for recursive lambda (due 6/19 24:00)