аспирант
Самара, Самарская область, Россия
сотрудник
ВАК 2.3.1 Системный анализ, управление и обработка информации, статистика
УДК 004.052.42 Обнаружение ошибок. Проверка достоверности данных. Верификация данных
Представлено исследование о варианте применения больших языковых моделей для верификации программного обеспечения. Цель: создание системы для автоматической верификации программного обеспечения заданным требованиям. Для достижения цели использованы информационные технологии, формальная верификация, искусственный интеллект и другие инновационные подходы. Методы: анализ современных инструментов и технологий для верификации ПО, включая существующие инструменты. Результаты: показывают сильные и слабые стороны применения больших языковых моделей для верификации ПО. Практическая значимость: заключается в повышении качества и надежности ПО. Исследование имеет важное значение для развития технологий железнодорожного транспорта и повышения надежности работы информационных систем. Обсуждение: высказываются рекомендации по дальнейшему совершенствованию предложенной системы верификации, освещаются вопросы, требующие дальнейших исследований и разработок.
большие языковые модели, формальная верификация, автоматизация спецификаций, Java Modeling Language, искусственный интеллект
1. 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).
2. 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:https://doi.org/10.1109/ICSE55347.2025.00129.
3. 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: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, 13 July 2021). New York: Association for Computing Machinery. 2021. Pp. 59–64. DOI:https://doi.org/10.1145/3464971.3468425.
5. 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: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 // 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:https://doi.org/10.1007/978-3-319-91908-9_18.
7. 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: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. 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:https://doi.org/10.48550/arXiv.2409.12866.
10. Code Llama: Open Foundation Models for Code / B. Rozière, J. Gehring, F. Gloeckle [et al.] // ArXiv. 2024. Vol. 2308.12950. 48 p. DOI:https://doi.org/10.48550/arXiv.2308.12950.
11. Qwen Technical Report / J. Bai, S. Bai, Y. Chu [et al.] // ArXiv. 2023. Vol. 2309.16609. 59 p. DOI:https://doi.org/10.48550/arXiv.2309.16609.
12. SpotBugs Manual — SpotBugs 4.9.8 Documentation. URL: http://spotbugs.readthedocs.io/en/latest/index.html (дата обращения: 07.11.2025).
13. About OpenJML. URL: http://www.openjml.org/about (дата обращения: 07.11.2025).
14. OpenJML Examples. URL: http://www.openjml.org/examples (дата обращения: 07.11.2025).
15. 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:https://doi.org/10.1007/978-3-031-90660-2_9.
