INTEGRATION OF LOGIC-ORIENTED VERIFICATION WITH LARGE LANGUAGE MODELS INTO SOFTWARE DEVELOPMENT
TL;DR
Experimental evaluation shows that increasing the proportion of successful verifications requires additional model training, a broader context, and the integration of mutation and candidate selection operations, while practical limitations of the proposed hybrid approach when using small-class models are identified.
Abstract
Background. Automating the generation of formal specifications remains one of the key tasks in formal software verification, as manual code annotation is labour-intensive and prone to errors. This paper proposes a hybrid approach combining locally deployed large language models (LLMs) and logical verification tools aimed at automatically generating JML annotations and their subsequent formal verification. The goal of the study is to evaluate the quality of the generated annotations and identify practical limitations of the approach when using small-class models. verification of annotations was performed using SpotBugs, and formal verification was performed using OpenJML in conjunction with the SMT solver Z3. The pipeline consists of four stages: automatic annotation generation, syntactic validation, deductive verification, and error classification with subsequent correction. The following metrics were used for evaluation: the proportion of syntactically correct annotations, the proportion of successfully verified specifications, and the processing time per class. Results. On a set of 11 examples, medium-sized OpenJML models demonstrated the ability to generate syntactically correct JML annotations, but the proportion of fully verified specifications remained low. The main limitations were identified in the area of semantic accuracy of annotations, the inability to take side effects into account, and, in some cases, the mismatch of formats between analysis tools. Experimental evaluation shows that increasing the proportion of successful verifications requires additional model training, a broader context, and the integration of mutation and candidate selection operations. Conclusions. The proposed hybrid approach demonstrates practical potential, but its implementation in real development will require improving the quality of the semantics of automatically generated contracts, expanding training sets, and creating automated error correction procedures integrated into the generation cycle.