기술 요약: 보간 기반 전이 불변량 생성을 통한 종료 분석

문제 정의

무한 상태 시스템의 종료(termination) 및 비종료(non-termination) 분석은 일반적으로 별개의 기법으로 다루어지는 상보적인 문제입니다. 종료를 증명하는 것은 종종 랭킹 함수(ranking functions)나 이산적 잘 정돈된 전이 불변량(disjunctively well-founded transition invariants)에 의존하는 반면, 비종료 분석은 주로 재귀 집합(recurrent sets, 실행으로부터 벗어날 수 없는 상태들의 집합)을 탐지하는 데 집중합니다. 안전성 기반 비종료 분석(Safety-based Non-termination Analysis, SNA)과 같은 기존 방식은 이들을 별개의 문제로 취급합니다. SNA는 안전성 문제를 반복적으로 정제하여 비종료를 증명하거나, 결론을 내릴 수 없을 경우 "UNKNOWN"을 반환하지만, 실패했을 때 종료를 증명할 수 있는 메커니즘은 부족합니다. 본 논문은 이 두 분석을 연결하여 중간 결과물을 공유하고 서로를 가이드할 수 있도록 하는 통합 프레임워크의 필요성을 다룹니다.

방법론

저자들은 크레이그 보간법(Craig interpolation)을 사용하여 잘 정돈된 전이 불변량을 생성함으로써 SNA를 확장하여 종료를 증명하는 통합 프레임워크를 제안합니다. 핵심 방법론은 다음 구성 요소들을 포함합니다:

1. 통합 프레임워크 아키텍처

이 접근 방식은 종료와 비종료 분석을 하나의 루프로 통합합니다. 이는 SNA가 구축한 종료 전이 궤적(terminating transition traces)(안전성 검사가 실패했을 때)을 구조적 정보의 원천으로 활용합니다. 단순히 이러한 궤적을 차단하여 안전성 문제를 정제하는 대신, 알고리즘은 이를 전이 불변량으로 일반화합니다.

2. 보간 기반 전이 불변량 생성 (TRINVGEN)

핵심 혁신은 종료 궤적으로부터 이산적으로 잘 정돈된 전이 불변량 후보를 생성하는 절차인 TRINVGEN입니다. 이 과정은 다섯 단계로 이루어집니다:

• $NT_n$의 계산: 알고리즘은 $n$번의 전이 내에 싱크 상태(non-sink states)에 도달할 수 있는 상태들을 인코딩하는 공식을 계산합니다.
• 보간(Interpolation): 궤적 공식과 $NT_n$의 부정(및 싱크 상태의 부정) 사이의 크레이그 보간량을 계산합니다. 이 보간량은 궤적을 과잉 근사하며 종료의 구조적 이유를 포착합니다.
• DNF 저차 근사(Under-approximation): 보간량을 논리곱 표준형(DNF) 공식으로 변환합니다. 지수적 폭발을 피하기 위해, SMT 솔버 모델을 기반으로 논리합(disjuncts)을 구성하는 온디맨드(on-demand) 방식을 사용합니다.
• 필터링(Filtering): 각 논리합에 대해 선형 랭킹 함수를 합성하여 잘 정돈됨(well-foundedness)을 확인합니다. 랭킹 함수를 허용하는 논리합만을 보존하여 후보 전이 불변량을 형성합니다.
• 커버리지 합성(Coverage Synthesis): 후보 전이 불변량이 유효한 상태들의 집합을 인코딩하는 커버리지 공식 $C(X)$를 계산합니다.

3. 반복 분석 및 자기 가이드(Self-Guidance)

메인 분석 루프(알고리즘 4 및 확장 알고리즘 5)는 다음과 같이 작동합니다:

• 안전성 검사(Safety Check): 시스템은 현재 문제에 대한 안전성 검사를 수행합니다.
• 불만족 케이스 (종료 궤적이 발견된 경우): 싱크 상태로의 궤적이 발견되면, TRINVGEN이 전이 불변량 후보와 커버리지 공식 $C$를 생성합니다.
  • 그 후, 불변량에 의해 커버되지 않는 상태($\neg C$)가 도달 가능한지 확인합니다.
  • $\neg C$가 도달 불가능하다면, 불변량이 모든 도달 가능한 상태를 커버하는 것이므로 시스템이 종료됨을 증명합니다.
  • $\neg C$가 도달 가능하다면, 알고리즘은 결정론적으로 종료를 유도하는 상태들을 차단(BLOCK-TERM)하여 문제를 정제하고, 커버되지 않은 상태들을 분석하기 위해 새로운 하위 문제들을 푸시합니다.
• 만족 케이스 (재귀 집합이 발견된 경우): 안전성 검사가 귀납적 불변량(inductive invariant)과 함께 "SAFE"를 반환하면, 알고리즘은 이 불변량이 재귀 집합인지 확인합니다. 만약 그렇다면, 시스템은 비종료 상태입니다.
• 스택 기반 확장 (알고리즘 5): 단일 불변량이 전체 상태 공간을 커버하지 못하는 복잡한 경우들을 처리하기 위해, 확장된 알고리즘은 안전성 문제의 스택을 유지합니다. 이는 현재 불변량이 유효하지 않은 특정 도달 가능 상태($S_m$)에 분석을 집중하여, 불변량을 확장하거나 해당 영역에 대한 비종료를 증명하려고 시도합니다.

주요 기여

본 논문은 세 가지 주요 기여를 제시합니다:

1. 새로운 보간 기반 생성법: 종료 이유를 포착하기 위해 크레이그 보간을 사용하여 이산적으로 잘 정돈된 전이 불변량을 생성하는 방법론을 제안합니다.
2. 통합 분석 절차: 종료와 비종료 분석을 통합하여, 중간 결과물(궤적 및 불변량)을 활용해 자기 가이드(self-guidance)를 수행하는 프레임워크를 제공합니다. 이를 통해 종료 증명은 커버되지 않은 상태에 집중할 수 있고, 비종료 증명은 종료 궤적의 구조적 통찰로부터 도움을 받을 수 있습니다.
3. 구현 및 평가: GOLEM 검증 프레임워크 내 구현 및 Termination Competition의 정수 전이 시스템(Integer Transition Systems) 벤치마크에 대한 평가를 수행했습니다.

실험 결과

저자들은 도구 ITPTIG+를 고전적 SNA, 중간 단계인 ITPTIG, 그리고 최첨단 도구들(KOAT, LOAT, T2)과 함께 1,200개의 정수 전이 시스템 벤치마크를 대상으로 평가했습니다.

• 고전적 SNA 대비 성능: ITPTIG+는 761개의 인스턴스를 해결하여, SNA(343개)와 ITPTIG(521개)를 크게 상회하는 성능을 보였습니다. 특히 SNA와 ITPTIG 모두 해결하지 못한 240개의 인스턴스를 독자적으로 해결했습니다.
• 최첨단 도구 대비 성능: T2가 전체적으로 가장 많은 인스턴스(1002개)를 해결했지만, ITPTIG+는 경쟁력 있는 성능을 보였으며 비교 대상 중 어떤 도구도 해결하지 못한 8개의 인스턴스를 독자적으로 해결했습니다. 특히, 두 개의 인스턴스(juLinkedListCreateAddAll.jar-obl-11 및 juLinkedListCreateAddAllAt.jar-obl-17)는 본 연구 이전까지 Termination Competition에서 어떤 도구도 해결하지 못했던 사례입니다.
• 비종료: 이 도구는 특정 미커버 상태 영역에 대한 재귀 집합 탐지에 집중함으로써 고전적 SNA에 비해 비종료 분석 측면에서 상당한 개선을 보여주었습니다.

의의 및 주장

본 논문은 종료와 비종료 추론을 결합하는 것이 유익하며, 최첨단 도구들과 대등한 성능을 내면서도 고유한 인스턴스들을 해결할 수 있다고 주장합니다. 이 연구의 의의는 이전에 분리되어 있던 두 문제를 단일 프레임워크 내에서 통합했다는 점에 있습니다. 크레이그 보간을 사용하여 종료 궤적을 일반화함으로써, 접근 방식은 종료의 구조적 이유를 포착하고 이를 전체 전이 시스템을 가이드하는 데 사용합니다. 저자들은 이 접근 방식을 안전성 검증에 기반을 둠으로써 견고한 토대를 제공하며, 이를 통해 기존의 안전성 솔버를 통해 두 속성을 모두 효율적으로 확인할 수 있음을 강조합니다. 본 연구는 한 유형의 분석(예: 실패한 안전성 검사로부터 얻은 궤적)에서 얻은 중간 결과가 다른 유형의 분석(예: 불변량 생성을 위한 종료 분석)을 효과적으로 구동할 수 있음을 입증하며, 이는 전체 검증 능력을 향상시키는 시너지 효과를 창출합니다.