作者位次 #2/10ACL 2026Workshop· ACL System Demonstrations
Formally Specifying the Intended Behavior of the Program: LLM -Driven Neuro-Symbolic Program Specification Synthesis
Cheng Wen · Hu Junjie · YiKun Hu · Jie Su · Bin Yu · Dugang Liu · Zhiwu Xu · Weidi Sun · Shengchao Qin · Cong Tian
摘要
Formal verification can provide strong mathematical guarantees about software correctness, but it typically requires developers to write detailed formal specifications (e.g., contracts and loop invariants), which is costly and error-prone. We introduce AutoSpec+, an LLM-driven neuro-symbolic demo...