Search papers, labs, and topics across Lattice.
SpecSyn addresses the challenge of automatically generating formal specifications for program verification by using LLMs to decompose programs into segments and iteratively generate specifications for each. It incorporates a novel specification refinement mechanism based on semantic-non-equivalent program mutations and variant discrimination to assess and enhance the semantic strength of the generated specifications. Experiments demonstrate that SpecSyn significantly outperforms existing LLM-based approaches, achieving over 90% precision and 75% recall, and successfully handling 1071 out of 1365 target properties for open-source programs.
LLMs can now automatically generate formal specifications for real-world programs with high precision and recall, thanks to a novel specification refinement mechanism that leverages program mutations.
Program verification is a formal technique to rigorously ensure the correctness and fault-freeness of software systems. However, constructing comprehensive interprocedural specifications for full verification obligations is time-consuming and labor-intensive, giving rise to automated specification generation approaches. Despite the significant advancements in these approaches brought by Large Language Models (LLMs), existing LLM-empowered approaches still suffer from significant limitations: they lack effective strategies for handling sizable input programs, and are typically equipped with no mechanisms to evaluate and guarantee the strength of the generated specifications. The limitations impair their ability to extract precise specifications from real-world complicated programs to support the verification of target properties, thereby hindering the applicability of existing approaches in verification tasks on real-world programs. To remedy this gap, we propose SpecSyn, a novel LLM-based specification generation method. SpecSyn first decomposes the input program into individual segments, which are handled respectively by the subsequent iterative specification generation process. Innovatively, we incorporate into the process a specification refinement mechanism based on semantic-non-equivalent program mutations and variant discrimination, assessing and enhancing the semantic strength of the generated specifications. Extensive experiments show that SpecSyn maintains high precision over 90% and outstanding recall over 75%, significantly outperforming existing LLM-based approaches. In further evaluations, SpecSyn successfully handles 1071 out of 1365 target properties for open-source programs, proving its applicability on real-world program verification tasks.
