Reading List on Program Analysis (SNU 4541.664A)

Kwangkeun Yi
Programming Research Laboratory/ Seoul National University

기본기/Preliminaries

지향/Orientation
의미구조 표현법/Semantic Formalism

Abstract Interpretation

Type-Based Analysis

Constraint-based Analysis

Software Model Checking

  • 요약 해석, 모델 검증, 자동 증명 기술을 모두 조합해서 MS의 device driver 소프트웨어 검증에 성공한 예: Automatic Predicate Abstraction of C Programs, 2001, Thomas Ball, Rupak Majundar, Todd Millstein and Sriram Rajamani
  • Model Checking, E. Clarke, O. Grumberg, and D. Peled, MIT Press, 2002

Etc.