аспирант с 01.01.2022 по 01.01.2025
Самара, Самарская область, Россия
сотрудник с 01.01.2016 по настоящее время
ВАК 1.2.1 Искусственный интеллект и машинное обучение
УДК 004.052.42 Обнаружение ошибок. Проверка достоверности данных. Верификация данных
Представлено исследование о варианте применения больших языковых моделей для верификации программного обеспечения. Цель: создание системы для автоматической верификации программного обеспечения заданным требованиям. Для достижения цели использованы информационные технологии, формальная верификация, искусственный интеллект и другие инновационные подходы. Методы: анализ современных инструментов и технологий для верификации ПО, включая существующие инструменты. Результаты: показывают сильные и слабые стороны применения больших языковых моделей для верификации ПО. Практическая значимость: заключается в повышении качества и надежности ПО. Исследование имеет важное значение для развития технологий железнодорожного транспорта и повышения надежности работы информационных систем. Обсуждение: высказываются рекомендации по дальнейшему совершенствованию предложенной системы верификации, освещаются вопросы, требующие дальнейших исследований и разработок.
JML, большие языковые модели, формальная верификация, автоматизация спецификаций, искусственный интеллект
1. Leavens G.T., Cheon Y. Design by Contract with JML. URL: https://www.cs.ucf.edu/~leavens/JML/jmldbc.pdf (Дата обращения: 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 (Дата обращения: 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 (Дата обращения: 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 Computing 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 (Дата обращения: 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 (Дата обращения: 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 (Дата обращения: 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 (Дата обращения: 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 (Дата обращения: 07.11.2025).
10. Roziere B. et al. Code Llama: Open Foundation Models for Code. URL: https://arxiv.org/abs/2308.12950 (Дата обращения: 07.11.2025).
11. Bai J. et al. Qwen Technical Report. URL: https://arxiv.org/abs/2309.16609 (Дата обращения: 07.11.2025).
12. SpotBugs manual URL: https://spotbugs.readthedocs.io/en/latest/index.html (Дата обращения: 07.11.2025).
13. About OpenJML URL: https://www.openjml.org/about/ (Дата обращения: 07.11.2025).
14. OpenJML Examples URL: https://www.openjml.org/examples/ (Дата обращения: 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 (Дата обращения: 07.11.2025).
