Reading List on Program Analysis (SNU 4541.664A)
지향/Orientation
의미구조 표현법/Semantic Formalism
- 좋은 개괄: Abstract
Interpretation: Achievements and Perspectives, 2000,
Patrick Cousot
- 좀더 긴: Abstract Interpretation Based Formal Methods and Future
Challenge, 2000, Patrick Cousot
- 더 긴: Abstract Interpretation Based Formal Methods and Future
Challenge, 2000, Patrick Cousot
- 오리지날 이론(정리되고 일반화되기 전, 하지만 대표적으로 읽어야 할):
Abstract
Interpretation: A Unified Lattice Model for Static Analysis of
Programs by Construction or Approximation of Fixpoints, 1977, Patrick
Cousot and Radhia Cousot
- 오리지날 이론2(오리지날과 함께 모든것이 다 말해졌다는): Systematic
Design of Program Analysis Frameworks, 1979, Patrick Cousot and Radhia Cousot
- 정리된 이론: Abstract
Interpretation Frameworks, 1992, Patrick Cousot and Radhia Cousot
- 축지법의 좋은 정리:
Comparing the Galois Connection and Widening/Narrowing Approaches to
Abstract Interpretation, 1992, Patrick Cousot and Radhia Cousot
- 참고로: Semantic Foundations of Program Analysis, 1981, Patrick Cousot
- 주마간산: Abstract
Interpretation, 1996, Patrick Cousot
- 요약 해석의 적용
- 요약 도메인의 다양한 예를 알고 싶다면: On Determining Lifetime and Aliasing of Dynamically Allocated Data in Higher-Order Functional Specification, 1990, Alain Deutsch
- 요약 해석의 한 예. 디자인 선택을 어떻게 하는지, 고정점 귀납을
이용한 증명은 어떤지 살펴보자: Compile-Time Detection of Uncaught Exceptions for Standard ML Programs, 1994, Kwangkeun Yi
- 요약 해석, 집합 제약식, 분석의 알갱이 조절 등이 총동원된 예:
A Cost-Effective Estimation of Uncaught Exceptions in Standard ML Programs, 2002, Kwangkeun Yi and Sukyoung Ryu
- 요약 해석을 AirBus 소프트웨어 검증에 이용한 예: A Static Analyzer for Large Safety-Critical Software, 2003, Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jerome Feret, Laurent Mauborgne, Antonie Mine, David Monniaux and Xavier Rival
- 요약 해석을 산업체 ANSI C 프로그램 검증에 적용한 예:
Airac, Taming False Alarms from a
Domain-Unaware C Analyzer by a Bayesian Statistical Post
Analysis, 2005,
Youngbum Jung, Jaehwang Kim, Jaeho Shin,
Kwangkeun Yi
- 동일화 알고리즘의 오리지날 논문:
A Machine-Oriented Logic Based on the
Resolution Principle, 1965, J. A. Robinson
- ML 타입 시스템의 준 오리지날 논문: Principal Type-schemes for Functional Programs, 1982, Luis Damas and Robin Milner
- 알기쉬운 ML 타입 시스템의 안전성 증명:
A Syntactic Approach to Type Soundness, 1994, Andrew K. Wright and Matthias Felleisen
- 타입 시스템에 올라타서 타입 이외의 것을 유추한 시초:
Polymorphic Type, Region and Effect
Inference, 1992, Jean-Pierre Talpin and Pierre Jouvelot
- 타입 시스템에 올라탄 분석의 힛트, 메모리 재활용 분석(region analysis):
Region-Based Memory Management,
1997, Mads Tofte and Jean-Pierre Talpin
- 또 다른 예, 프로그램이 단조증가하는 함수이냐를 검증하는 분석: Static Monotonicity Analysis for Lambda-definable Functions over Lattices, 2002, Andrzej Murawski and Kwangkeun Yi
- 타입 유추 알고리즘들의 다양한 변형에 대해 알고 싶다면: Proofs about a Folklore Let-Polymorphic Type Inference Algorithm, 1998, Oukseh Lee and Kwangkeun Yi
- 집합 제약식을 이용한 분석의 개괄 (비평적으로 읽기)
Introduction to Set Constraint-Based
Program Analysis, 1999, Alex Aiken
(PLDI 튜토리얼 슬라이드, 1995, Alex
Aiken and Nevin Heintze)
- 집합 제약식을 이용한 ML 프로그램 분석 예: Set Based Analysis of ML Programs, 1994, Nevin Heintze
- 집합 제약식을 이용한 분석 틀을 잡은 학위 논문: Set Based Program Analysis, 1992, Nevin Heintze
- 집합 제약식의 해를 구하는 알고리즘 (제한된, 하지만 대게의
프로그램분석에서 유용한) A Decision
Procedure for a Class of Set Constraints, 1991, Nevin Heintze and
Joxan Jaffar (short version)
- 요약 해석, 모델 검증, 자동 증명 기술을 모두 조합해서 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
|
|