이진 탐색을 이용하는 단계 고정점 계산 가속 기법을 통한 C 프로그램 정적 분석 정확도 개선

Abstract

이 논문은 구간 도메인(interval domain)을 이용하는 정적 분석에서 보다 정교 하고 효율적인 고정점 계산 가속 기법(widening)을 이용하여 분석 정확도를 개선하 는 방법을 제시한다. 기본적인 고정점 계산 가속 기법(conventional widening)[1]은 반복문에서 나타나는 변수들을 과도하게 추정하여 계산하는데, 이는 허위 경보의 원인 중 하나이다. 이로 인해 발생하는 허위 경보들은 더 정교하게 계산하는 고정점 계산 가속 기법(widening) 이외의 다른 방법으로는 줄이기 어려우며, 이를 실험으로 보이고자 한다. 단계 고정점 계산 가속 기법(thresholded widening)[2]을 이용하면 기본적인 고정점 계산 가속 기법(conventional widening)으로 인해 발생하는 허위 경보들을 줄일 수 있다. 하지만 단계 고정점 계산 가속 기법(thresholded widening) 은 추가 비용이 크며 이를 줄이기 위한 방법으로 이진 탐색을 적용하는 방법을 소 개하고자 한다. 이 논문에서는 이진 탐색을 이용하는 단계 고정점 계산 가속 기법 (thresholded widening using binary search) 및 분석 디자인을 소개하고, 이로 인해 허위경보가 줄어드는 것을 실험을 통해 보인다.