A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
본 논문은 정적 분석과 LLM 기반 추론을 결합한 모듈형 프레임워크인 Preguss 를 통해 대규모 프로그램의 잠재적 런타임 오류를 기반으로 인터프로시저 명세를 자동 생성 및 정제함으로써, 기존 LLM 기반 접근법보다 우수한 확장성을 보이며 수천 줄 규모의 프로그램에 대한 검증 노력을 80.6%~88.9% 감소시킨다고 제안합니다.