AI RESEARCH
Evaluating LLM-Generated ACSL Annotations for Formal Verification
arXiv CS.AI
•
ArXi:2602.13851v2 Announce Type: replace-cross Formal specifications are crucial for building verifiable and dependable software systems, yet generating accurate and verifiable specifications for real-world C programs remains challenging. This paper empirically evaluates the extent to which formal-analysis tools can automatically generate and verify ACSL specifications without human or learning-based assistance. We conduct a controlled study on a recently released dataset of 506 C programs, repurposing it from interactive, developer-driven workflows to an automated evaluation setting.