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 Frameworks, 1992, Patrick Cousot and Radhia 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
- 축지법의 좋은 정리:
Comparing the Galois Connection and Widening/Narrowing Approaches to
Abstract Interpretation, 1992, Patrick Cousot and Radhia Cousot
- 실행궤적 나누기(trace partitioning): 프로그램의 실행궤적(trace)들을
요약하는 일반적인 방법
Trace Partitioning in
Abstract Interpretation Based Static Analyzers, 2005,
L. Mauborgne and X. Rival
- 참고로: Semantic Foundations of Program Analysis, 1981, Patrick Cousot
- 주마간산: Abstract
Interpretation, 1996, Patrick Cousot
- 100만라인 C 프로그램을 통째로 자세하고 안전하게 분석하는 이론과
실제:
Design and Implementation of Sparse Global Analyses for
C-like Languages, 2012, Hakjoo Oh, Kihong Heo, Wonchan Lee,
Woosuk Lee, Kwangkeun Yi. PLDI
- 프로그램이 프로그램을 만들고 실행하는 경우의 분석기술:
Static Analysis for Multi-Staged
Programs via Unstaging Translation, 2011,
Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto
Tatsuda. POPL
- 요약 도메인의 다양한 예를 알고 싶다면: On Determining Lifetime and Aliasing of
Dynamically Allocated Data in Higher-Order Functional
Specification, 1990, Alain Deutsch. PLDI
- 요약 해석의 한 예. 디자인 선택을 어떻게 하는지, 고정점 귀납을
이용한 증명은 어떤지 살펴보자: Compile-Time Detection of
Uncaught Exceptions for Standard ML Programs, 1994, Kwangkeun
Yi. SCP
- 요약 해석, 집합 제약식, 분석의 알갱이 조절 등이 총동원된 예:
A Cost-Effective Estimation
of Uncaught Exceptions in Standard ML Programs, 2002, Kwangkeun
Yi and Sukyoung Ryu. TCS
- 요약 해석을 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. PLDI
- 요약 해석을 산업체 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. SAS
- 동일화 알고리즘의 오리지날 논문:
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)
|
|