AutoACSL: LLM과 CPG 기반 정적 분석의 통합을 통한 ACSL 명세 합성

C 프로그램에 대한 형식 명세(formal specifications)를 생성하는 것은 요구되는 수동 작업, 전문 지식 및 의미론적 정밀도(semantic precision)로 인해 형식 검증(formal verification) 분야에서 여전히 어려운 과제로 남아 있습니다. 최근 대규모 언어 모델(LLMs)의 발전이 명세 합성(specification synthesis) 자동화에 가능성을 제시하고 있지만, 현재의 접근 방식은 종종 의미론적 깊이가 부족하며 검증 불가능하거나 불완전한 계약(contracts)을 생성합니다. 이러한 한계를 해결하기 위해, 우리는 LLM 프롬프팅(prompting)을 코드 속성 그래프(Code Property Graphs, CPGs)에서 추출된 의미론적 특징과 통합하는 새로운 프레임워크인 AutoACSL을 소개합니다. AutoACSL은 정적 분석(static analyses)을 수행하여 산술 연산, 루프 및 재귀 구조, 반환 값 전파(return value propagation)를 포함한 핵심 의미론적 요소를 추출하며, 이는 구조화된 프롬프트로 인코딩됩니다. 이러한 프롬프트를 통해 LLM은 일반적인 동작 명세를 생성할 뿐만 아니라, 런타임 에러(runtime errors)를 유발하는 입력을 방지하는 제약 조건(constraints)을 포함할 수 있습니다. AutoACSL은 피드백 기반 합성 루프(feedback-driven synthesis loop)를 채택하여, 후보 명세를 Frama-C/WP를 사용하여 검증하고 검증에 성공하거나 종료 조건이 충족될 때까지 반복적으로 개선합니다. 다양한 데이터셋에서 추출한 604개의 프로그램을 대상으로 평가한 결과, AutoACSL은 Gemini-3와 결합했을 때 98%의 명세 생성 성공률과 96%의 완전 증명 비율(full proof ratio)을 달성했습니다. 코드 전용 베이스라인(code-only baseline)과 비교했을 때, AutoACSL은 4개의 LLM(GPT-o4 Mini, GPT-5.2, Grok-4.1, Gemini-3) 전반에서 완전 증명 비율을 24.7%에서 51.7%까지 향상시켰으며, 이는 대규모 언어 모델을 CPG 기반 정적 분석과 통합하는 것이 자동화된 ACSL 명세 합성을 위한 생성 견고성(generation robustness)과 검증 효과성(verification effectiveness)을 실질적으로 향상시킨다는 것을 입증합니다.