양방향 정적분석을 통한 정수구간 명세 자동유추의 실험

Abstract

프로그램 검증에서 정적 분석은 명세를 자동으로 유추하고 안전성을 보장한다. 하지만 전조건에 대한 명세를 잘 유추하지 못한다. 전조건을 유추하면 시작 지점을 알 수 없는 프로그램에도 의미 있는 결과를 유추할 수 있다. 앞선 논문에서는 기존 정적분석 이론을 변형하여 정수구간의 전조건을 유추하는 안전한 양방향 정적 분석기를 설계하였지만 실제 실험 결과 정확한 전조건을 얻지 못했다. 본 논문에서는 안전성을일부 포기하는 대신 정확한 전조건을 얻기 위한 휴리스틱을 적용하였다. 그 결과 특정 경우 배열 인덱스범위에 대한 정확한 전조건을 구할 수 있었다.