Intellectual Technologies on Transport Intellectual Technologies on Transport Интеллектуальные технологии на транспорте 2413-2527 106708 10.20295/2413-2527-2025-444-47-53 srwdxj ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ И ТРАНСПОРТНЫЕ СИСТЕМЫ ARTIFICIAL INTELLIGENCE AND TRANSPORT SYSTEMS ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ И ТРАНСПОРТНЫЕ СИСТЕМЫ Formal Verification of Software Using Large Language Models Формальная верификация программного обеспечения с помощью больших языковых моделей Мельников Павел Андреевич Melnikov Pavel Andreevich gleavero@gmail.com https://orcid.org/0000-0002-0329-2163 Тюгашев Андрей Александрович Tyugashev Andrey Aleksandrovich tau797@mail.ru

доктор технических наук;

doctor of technical sciences;

 Институт автоматики и информационных технологий, Самарский государственный технический университет Самара Россия Automation and Information Technology Institute, Samara State Technical University Samara Russian Federation Институт автоматики и информационных технологий, Самарский государственный технический университет Самара Россия Automation and Information Technology Institute, Samara State Technical University Samara Russian Federation 15 12 2025 15 12 2025 4 47 53 15 11 2025 18 11 2025 https://itt-pgups.ru/en/nauka/article/106708/view

Представлено исследование о варианте применения больших языковых моделей для верификации программного обеспечения. Цель: создание системы для автоматической верификации программного обеспечения заданным требованиям. Для достижения цели использованы информационные технологии, формальная верификация, искусственный интеллект и другие инновационные подходы. Методы: анализ современных инструментов и технологий для верификации ПО, включая существующие инструменты. Результаты: показывают сильные и слабые стороны применения больших языковых моделей для верификации ПО. Практическая значимость: заключается в повышении качества и надежности ПО. Исследование имеет важное значение для развития технологий железнодорожного транспорта и повышения надежности работы информационных систем. Обсуждение: высказываются рекомендации по дальнейшему совершенствованию предложенной системы верификации, освещаются вопросы, требующие дальнейших исследований и разработок.

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.

 большие языковые модели формальная верификация автоматизация спецификаций Java Modeling Language искусственный интеллект large language models formal verification specification automation Java Modeling Language artificial intelligence

Leavens G. T., Cheon Y. Design by Contract with JML. 2006. 13 p. URL: http://www.academia.edu/26405390/Design_by_Contract_with_JML (дата обращения: 07.11.2025). 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). SpecGen: Automated Generation of Formal Program Specifications via Large Language Models / L. Ma, S. Liu, Y. Li // Proceedings of the 47th International Conference on Software Engineering (ICSE 2025) (Ottawa, Canada, 26 April — 06 May 2025). Institute of Electrical and Electronics Engineers, 2025. Pp. 16–28. DOI: 10.1109/ICSE55347.2025.00129. 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: 10.1109/ICSE55347.2025.00129. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? / M. Endres, S. Fakhoury, S. Chakraborty, S. K. Lahiri // Proceedings of the ACM on Software Engineering. 2024. Vol. 1, Iss. FSE. Art. No. 84. Pp. 1889–1912. DOI: 10.1145/366079. 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: 10.1145/366079. 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, 13 July 2021). New York: Association for Computing Machinery. 2021. Pp. 59–64. DOI: 10.1145/3464971.3468425. 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: 10.1145/3464971.3468425. The Java Verification Tool KeY: A Tutorial / B. Beckert, R. Bubel, D. Drodt [et al.] // Formal Methods (FM 2024): Proceedings of the 26th International Symposium (Milan, Italy, 09–13 September 2024). Part 2. Lecture Notes in Computer Science. Vol. 14934 / A. Platzer [et al.] (eds). Cham: Springer, 2025. Pp. 597–623. DOI: 10.1007/978-3-031-71177-0_32. 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: 10.1007/978-3-031-71177-0_32. Hähnle R., Huisman M. Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools // Computing and Software Science: State of the Art and Perspectives. Lecture Notes in Computer Science. Vol. 10000 / B. Steffen, G. Woeginger (eds). Cham: Springer, 2019. Pp. 345–373. DOI: 10.1007/978-3-319-91908-9_18. 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: 10.1007/978-3-319-91908-9_18. Modular Verification of JML Contracts Using Bounded Model Checking / B. Beckert, M. Kirsten, J. Klamroth, M. Ulbrich // 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, 20–30 October 2020). Part 1. Lecture Notes in Computer Science. Vol. 12476 / T. Margaria, B. Steffen (eds). Cham: Springer, 2020. Pp. 60–80. DOI: 10.1007/978-3-030-61362-4_4. 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: 10.1007/978-3-030-61362-4_4. 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: 10.5445/IR/1000084545. 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: 10.5445/IR/1000084545. SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications / L. Ma, S. Liu, L. Bu [et al.] // ArXiv. 2025. Vol. 2409.12866. 12 p. DOI: 10.48550/arXiv.2409.12866. 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: 10.48550/arXiv.2409.12866. Code Llama: Open Foundation Models for Code / B. Rozière, J. Gehring, F. Gloeckle [et al.] // ArXiv. 2024. Vol. 2308.12950. 48 p. DOI: 10.48550/arXiv.2308.12950. Rozière B., Gehring J., Gloeckle F., et al. Code Llama: Open Foundation Models for Code, ArXiv, 2024, Vol. 2308.12950, 48 p. DOI: 10.48550/arXiv.2308.12950. Qwen Technical Report / J. Bai, S. Bai, Y. Chu [et al.] // ArXiv. 2023. Vol. 2309.16609. 59 p. DOI: 10.48550/arXiv.2309.16609. Bai J., Bai S., Chu Y., et al. Qwen Technical Report, ArXiv, 2023, Vol. 2309.16609, 59 p. DOI: 10.48550/arXiv.2309.16609. SpotBugs Manual — SpotBugs 4.9.8 Documentation. URL: http://spotbugs.readthedocs.io/en/latest/index.html (дата обращения: 07.11.2025). SpotBugs Manual — SpotBugs 4.9.8 Documentation. Available at: http://spotbugs.readthedocs.io/en/latest/index.html (accessed: November 07, 2025). About OpenJML. URL: http://www.openjml.org/about (дата обращения: 07.11.2025). About OpenJML. Available at: http://www.openjml.org/about (accessed: November 07, 2025). OpenJML Examples. URL: http://www.openjml.org/examples (дата обращения: 07.11.2025). OpenJML Examples. Available at: http://www.openjml.org/examples (accessed: November 07, 2025). Beyer D., Strejček J. Improvements in Software Verification and Witness Validation: SV-COMP // Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025): Proceedings of the 31st International Conference (Hamilton, Canada, 03–08 May 2025). Part 3. Lecture Notes in Computer Science. Vol. 15698 / A. Gurfinkel, M. Heule (eds). Cham: Springer, 2025. Pp. 151–186. DOI: 10.1007/978-3-031-90660-2_9. 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: 10.1007/978-3-031-90660-2_9.