Frama-C

深度分析

LLM 生成 ACSL 標註於 C 程式驗證之效能評估與比較分析

本研究針對 C 程式的形式驗證，評估規則式腳本、Frama‑C RTE 外掛與三款 LLM 產生的 ACSL 標註。實驗以 CASP 基準子集透過 Frama‑C WP 與 SMT 求解器測試證明成功率與執行時間。結果顯示規則式方法較為可靠，LLM 表現波動，顯示其潛在輔助價值。