graduate student from 01.01.2022 to 01.01.2025
Samara, Samara, Russian Federation
employee from 01.01.2016 until now
VAK Russia 1.2.1
UDC 004.052.42
This paper presents a study on the application of large language models (LLMs) for software verification. The main objective of the study is to create a system for automatic verification of software against specified requirements. To achieve this goal, information technology, formal verification, artificial intelligence, and other innovative approaches are used. Research method: analysis of modern tools and technologies, including existing tools for software verification. The results of the study show the strengths and weaknesses of using LMMs for software verification. The practical significance lies in improving the quality and reliability of software. The discussion provides recommendations for further improvement of the proposed verification system and highlights issues that require further research and development. The study is important for the development of railway transport technologies and improving the reliability of information systems.
JML, large language models, formal verification, specification automation, artificial intelligence
1. L Leavens G.T., Cheon Y. Design by Contract with JML. URL: https://www.cs.ucf.edu/~leavens/JML/jmldbc.pdf (accessed: 07.11.2025).
2. Ma L. et al. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. URL: https://arxiv.org/abs/2401.08807 (accessed: 07.11.2025).
3. Endres M. et al. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? URL: https://arxiv.org/abs/2310.01831 (accessed: 07.11.2025).
4. Armand Puccetti, Gaël de Chalendar, and Pierre-Yves Gibello. 2021. Combining formal and machine learning techniques for the generation of JML specifications. In Proceedings of the 23rd ACM Interna-tional Workshop on Formal Techniques for Java-like Programs (FTfJP '21). Association for Compu-ting Machinery, New York, NY, USA, 59-64.
5. Beckert, B. et al. The Java Verification Tool KeY:A Tutorial. URL: https://doi.org/10.1007/978-3-031-71177-0\_32 (accessed: 06.11.2025)
6. Hähnle, R., Huisman, M. Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. URL: https://doi.org/10.1007/978-3-319-91908-9_18 (accessed: 06.11.2025)
7. Beckert, B., Kirsten, M., Klamroth, J., Ulbrich, M. Modular Verification of JML Contracts Using Bounded Model Checking. URL: https://doi.org/10.1007/978-3-030-61362-4_4 (accessed: 06.11.2025)
8. Liu, T. Efficient Verification of Programs with Complex Data Structures Using SMT Solvers. URL: https://doi.org/10.5445/IR/1000084545 (accessed: 06.11.2025).
9. Ma L. et al. SpecEval: Evaluating Code Comprehension in Large Language Models via Program Speci-fications. URL: https://arxiv.org/abs/2409.12866 (accessed: 07.11.2025).
10. Roziere B. et al. Code Llama: Open Foundation Models for Code. URL: https://arxiv.org/abs/2308.12950 (accessed: 07.11.2025).
11. Bai J. et al. Qwen Technical Report. URL: https://arxiv.org/abs/2309.16609 (accessed: 07.11.2025).
12. SpotBugs manual URL: https://spotbugs.readthedocs.io/en/latest/index.html (accessed: 07.11.2025).
13. About OpenJML URL: https://www.openjml.org/about/ (accessed: 07.11.2025).
14. OpenJML Examples URL: https://www.openjml.org/examples/ (accessed: 07.11.2025).
15. Beyer D., Jan Strejcek Improvements in Software Verification and Witness Validation: SV-COMP 2025. URL: https://www.sosy-lab.org/research/pub/2025-TACAS.Improvements_in_Software_Verification_and_Witness_Validation_SV-COMP_2025.pdf (accessed: 07.11.2025).
