AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis

AutoACSL is a new framework that combines large language models (LLMs) with Code Property Graphs (CPGs) to automate the synthesis of ACSL specifications for C programs. It utilizes static analysis to extract semantic features and generates structured prompts for LLMs, leading to a 98% success rate in specification generation and a 96% verification success with Frama-C/WP, significantly improving proof ratios by up to 51.7% compared to traditional code-only methods. This integration enhances the robustness and effectiveness of automated specification generation, which is crucial for practitioners involved in formal verification processes.