팔각형 추상 도메인 (Octagonal Abstract Domains)의 최소 비교

수치적 추상 도메인 (Numerical abstract domains)은 그 표현력 (expressiveness)에 따라 다양합니다. Zones와 같이 더 표현력이 높은 도메인은 Intervals보다 더 정밀한 불변량 (invariants)을 산출합니다. 추상 도메인을 선택하기 위한 포괄적인 접근 방식은 추상 상태 (abstract states)의 최소 비교 (minimal comparison)입니다. 그러나 이것이 효과를 거두려면 추상 상태가 가짜 제약 조건 (spurious constraints)으로부터 자유로워야 합니다. 이전 연구들이 Zones를 위한 가짜 제약 조건 제거 기법을 개발했다면, 본 연구는 Octagons에 대해 이러한 제약 조건을 제거하기 위한 새로운 알고리즘을 소개합니다. 우리는 서로 다른 추상 도메인으로부터 얻은 6,930개의 불변량의 정밀도를 비교함으로써 우리의 접근 방식을 평가합니다. 연구 결과, 최소 비교를 통해 많은 불변량이 동등한 것으로 재분류되었으며, 이를 통해 Octagons의 표현력이 불변량 정밀도에 미치는 영향을 줄일 수 있음을 보여줍니다.