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이라고 한다.