필요한 부위, 시점, 상황 선별을 통한 프로그램 전체 분석의 비용 절감 기술

Abstract

In this dissertation we present general methods for achieving sound, precise, and also scalable global static analyzers. We first use the abstract interpretation framework to have a sound and precise global staic analyzer whose scalability is not yet attended. Then, we add our localization techniques to improve its scala- bility while preserving the precision and soundness of the underlying analysis. We present three localization techniques that allow the analysis to concentrate on rel- evant portions of spatial, temporal, and contextual states, respectively. The tech- niques are successfully applied to an industrial-strength C static analyzer to scale to analyze up to one million lines of C programs.