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

Abstract

프로그램 검증에 있어, 정적 프로그램 분석은 명세를 자동으로 유추한다는 점에서 자동 증명기와는 다른 특별한 위치를 지닌다. 자동 유추는 효율성 면에서 매우 중요한 요소인데, 기존 정형검증 방법이 일정 경우 사용자 조작을 필요로 하는 반자동 방식이기 때문에 대규모 프로그램의 경우 검증시간을 단축하는 자동인 방법이 필요하다. 정적 프로그램 분석은 사용자가 직접 요약된 의미를 기술해야 하는 모델검증이나 불변식과 같은 인자를 제공해야 하는 자동 증명기와 달리, 요약해석이라는 수학적 개념구조를 이용해 가능한 프로그램 상태를 안전하면서도 자동으로 추정한다. 그러나 이런 자동명세의 장점에도 불구하고 정적 분석은 후조건은 쉽게 유추할 수 있지만 전조건은 잘 유추하지 못한다는 문제점이 있다. 후조건 유추는 시작지점에서부터 연역적으로 추론해나가므로 결과가 결정적이지만, 전조건 유추는 후조건이 주어졌을 때 가능한 전제조건을 추론하기 때문에 더 많은 불확실성을 가진다. 이런 불확실성은 요약해석 구조 안에서 보장 될 수 있는 안전성, 정확성과 같은 여러 성질을 위협할 수 있어 그 동안 분석 분야에서 잘 시도되지 않았다. 만약 전조건을 효율적으로 유추 할 수 있다면 프로그램을 부분만 보고도 결론을 낼 수 있는 조립적인 분석기를 만들 수 있다. 후조건을 유추하는 기존 분석기는 이벤트 기반과 같은 시작지점이 없는 프로그램의 경우 결과를 제대로 유추하지 만약 전조건을 유추할 수 있다면 시작지점을 모르거나 부분만 아는 프로그램도 의미있는 결과를 유추할 수 있다. 본 연구에서는 정수구간 도메인에 한해 기존 정적 분석을 변형하여 자동으로 전조건을 유추하는 방법을 제안한다. 기존 구간 분석은 후조건을 수집하는 방향으로 개발되어 왔으며 전조건을 유추하는 방법은 제시된 바 없다. 우리는 분석기의 안전성을 만족하면서 정수 구간 전조건을 유추할 수 있는 새로운 분석기를 제안한다.