공유 컨텍스트 배치 충족 가능성 (Shared-Context Batched Satisfiability)

프로그램 분석기(Program analyzers)는 종종 대규모의 심볼릭 컨텍스트(symbolic context)를 공유하며 오직 작은 술어(predicate)만 서로 다른 SMT 쿼리들을 배치(batch) 형태로 발행합니다. 우리는 이러한 반복되는 패턴을 extit{공유 컨텍스트 배치 충족 가능성 (Shared-Context Batched Satisfiability)}으로 공식화합니다: 공식 $\varphi$와 술어 집합 $P$가 주어졌을 때, 각 $p \in P$에 대하여 $\varphi \land p$가 충족 가능한지(satisfiable)를 결정하는 문제입니다. 우리는 이 문제에 대해 세 가지 이론 불가지론적(theory-agnostic) 전략을 연구합니다: 술어별 확인(predicate-by-predicate checking), 논리합 과잉 근사(disjunctive over-approximation), 그리고 $\varphi$와 일치하지 않는 리터럴(literals)을 학습하여 이후의 술어들을 거부하는 데 사용하는 새로운 알고리즘인 코어 리터럴 필터(Core-Literal Filter, CLF)입니다. 심볼릭 추상화(symbolic abstraction) 및 능동적 속성 검사(active property checking)에 대한 평가 결과, 어떤 전략도 보편적으로 우세하지 않음을 보여줍니다: 과잉 근사(over-approximation)는 해결된 심볼릭 추상화 쿼리에서 가장 빠르며, CLF는 해결된 어려운 인스턴스의 수를 증가시키고 능동적 속성 검사에서 가장 빠릅니다. 우리는 공유 컨텍스트 배치 충족 가능성을 프로그램 분석기 설계 시 일급 프리미티브(first-class primitive)로 취급하고, 알고리즘 설계 공간을 더욱 체계적으로 탐색할 것을 권장합니다.