SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications
Formal specifications are essential for deductive program verification, providing semantic abstractions for compositional verification of complex software. However, manually constructing specifications is labor-intensive, motivating automated synthesis. Despite recent advances in large language models (LLMs), existing...