Abstract interpretation 문서 원본 보기

[[분류: 프로그램 분석]]

== 개요 ==
Abstract Interpretation이란, 프로그램을 Soundess를 충족하는 Abstraction(추상화)를 만들어서 Program을 검증하는 것이다. Abstract Interpretation은 [[Static analysis]]를 구현하는 이론적인 토대가 되어서, Compiler에서 프로그램의 Optimization이나, Verifier에서 프로그램의 문제를 분석하는 것에 사용된다.

프로그램을 Concrete한 정보를 가지고 분석하는 일은 불가능 할 뿐더러 ([[Halting problem]], [[Rice's theorem]]참고), Limitation을 두더라도 매우 오래 걸리는 힘든 일이다. 따라서 프로그램 분석을 위한 정도로 프로그램을 Abstract시켜서, 비록 [[Complete]]한 결과는 아니지만, [[Sound]]한 결과를 도출해 내도록 단순화시켜 분석하는 작업을 Abstraction이라고 한다.