SpecGen: Automated Generation of Formal Program Specifications via Large Language Models

• DOI: 10.48550/arxiv.2401.08807
• Publication Date: 2024-01-01
• Authors: Lezhi Ma; Shangqing Liu; Yi Li; Xiaofei Xie; Lei Bu
• Keywords: Programming language specification

Formal program specifications play a crucial role in various stages of software development. However, manually crafting formal is rather difficult, making the job time-consuming and labor-intensive. It even more challenging to write that correctly comprehensively describe semantics complex programs. To reduce burden on developers, automated specification generation methods have emerged. existing usually rely predefined templates or grammar, them struggle accurately behavior functionality real-world tackle this challenge, we introduce SpecGen, novel technique for based Large Language Models. Our key insight overcome limitations by leveraging code comprehension capability LLMs. The process SpecGen consists two phases. first phase employs conversational approach guides LLM generate appropriate given program. second phase, designed where fails correct specifications, applies four mutation operators model-generated selects verifiable from mutated ones through heuristic selection strategy. We evaluate datasets, including SV-COMP Java category benchmark constructed dataset. Experimental results demonstrate succeeds generating 279 out 385 programs, outperforming purely LLM-based approaches conventional tools like Houdini Daikon. Further investigations quality generated indicate can articulate behaviors input