graduate student
Samara, Samara, Russian Federation
employee
VAK Russia 2.3.1
UDC 004.052.42
This study presents an exploration of the application of large language models for software verification. Purpose: to create a system for the automatic verification of software for specified requirements. Information technologies, formal verification, artificial intelligence, and other innovative approaches have been used to achieve this goal. Methods: analysis of current tools and technologies for software verification, including existing instruments. Results: the research highlights the strengths and weaknesses associated with the use of large language models for software verification. Practical significance: enhancing the quality and reliability of software is crucial. This research is important for advancing railway transportation technologies and increasing the reliability of information systems. Discussion: recommendations have been formulated for further improvement of the proposed verification system. Additionally, the issues requiring further research and development have been highlighted.
large language models, formal verification, specification automation, Java Modeling Language, artificial intelligence
1. Leavens G. T., Cheon Y. Design by Contract with JML. 2006. 13 p. Available at: http://www.academia.edu/26405390/Design_by_Contract_with_JML (accessed: November 07, 2025).
2. Ma L., Liu S., Li Y. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models, Proceedings of the 47th International Conference on Software Engineering (ICSE 2025), Ottawa, Canada, April 26 — May 06, 2025. Institute of Electrical and Electronics Engineers, 2025, Pp. 16–28. DOI:https://doi.org/10.1109/ICSE55347.2025.00129.
3. Endres M., Fakhoury S., Chakraborty S., Lahiri S. K. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? Proceedings of the ACM on Software Engineering, 2024, Vol. 1, Iss. FSE, Art. No. 84, Pp. 1889–1912. DOI:https://doi.org/10.1145/366079. EDN: https://elibrary.ru/HTFJZS
4. Puccetti A., de Chalendar G., Gibello P.-Y. Combining Formal and Machine Learning Techniques for the Generation of JML Specifications, Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP ‘21), Online, July 13, 2021. New York, Association for Computing Machinery, 2021, Pp. 59–64. DOI:https://doi.org/10.1145/3464971.3468425.
5. Beckert B., Bubel R., Drodt D., et al. The Java Verification Tool KeY: A Tutorial. In: Platzer A., et al. (eds) Formal Methods (FM 2024): Proceedings of the 26th International Symposium, Milan, Italy, September 09–13, 2024. Part 2. Lecture Notes in Computer Science. Vol. 14934. Cham, Springer, 2025, Pp. 597–623. DOI:https://doi.org/10.1007/978-3-031-71177-0_32.
6. Hähnle R., Huisman M. Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. In: Steffen B., Woeginger G. (eds) Computing and Software Science: State of the Art and Perspectives. Lecture Notes in Computer Science. Vol. 10000. Cham, Springer, 2019, Pp. 345–373. DOI:https://doi.org/10.1007/978-3-319-91908-9_18.
7. Beckert B., Kirsten M., Klamroth J., Ulbrich M. Modular Verification of JML Contracts Using Bounded Model Checking, In: Margaria T., Steffen B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles (ISoLA 2020): Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Rhodes, Greece, October 20–30, 2020. Part 1. Lecture Notes in Computer Science. Vol. 12476. Cham, Springer, 2020, Pp. 60–80. DOI:https://doi.org/10.1007/978-3-030-61362-4_4.
8. Liu T. Efficient Verification of Programs with Complex Data Structures Using SMT Solvers: A Thesis for the Degree of Doctor of Natural Science. Karlsruhe Institute of Technology, 2018, 173 p. DOI:https://doi.org/10.5445/IR/1000084545.
9. Ma L., Liu S., Bu L., et al. SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications, ArXiv, 2025, Vol. 2409.12866, 12 p. DOI:https://doi.org/10.48550/arXiv.2409.12866.
10. Rozière B., Gehring J., Gloeckle F., et al. Code Llama: Open Foundation Models for Code, ArXiv, 2024, Vol. 2308.12950, 48 p. DOI:https://doi.org/10.48550/arXiv.2308.12950.
11. Bai J., Bai S., Chu Y., et al. Qwen Technical Report, ArXiv, 2023, Vol. 2309.16609, 59 p. DOI:https://doi.org/10.48550/arXiv.2309.16609.
12. SpotBugs Manual — SpotBugs 4.9.8 Documentation. Available at: http://spotbugs.readthedocs.io/en/latest/index.html (accessed: November 07, 2025).
13. About OpenJML. Available at: http://www.openjml.org/about (accessed: November 07, 2025).
14. OpenJML Examples. Available at: http://www.openjml.org/examples (accessed: November 07, 2025).
15. Beyer D., Strejček J. Improvements in Software Verification and Witness Validation: SV-COMP. In: Gurfinkel A., Heule M. (eds) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025): Proceedings of the 31st International Conference, Hamilton, Canada, May 03–08, 2025. Part 3. Lecture Notes in Computer Science. Vol. 15698. Cham, Springer, 2025, Pp. 151–186. DOI:https://doi.org/10.1007/978-3-031-90660-2_9.
