Details
Title | Формальные спецификации для аппроксимации поведения функций стандартной библиотеки: научный доклад: направление подготовки 09.06.01 «Информатика и вычислительная техника» ; направленность 09.06.01_06 «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей» |
---|---|
Creators | Онищук Михаил Петрович |
Scientific adviser | Дробинцев Павел Дмитриевич |
Organization | Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и кибербезопасности |
Imprint | Санкт-Петербург, 2024 |
Collection | Научные работы аспирантов/докторантов ; Общая коллекция |
Subjects | Системное программное обеспечение ; стандартная библиотека языка ; формальные спецификации библиотек ; моделирование поведения библиотеки ; статический анализ программ ; генерация тестов ; standard library ; formal specifications ; library behavior modeling ; static program analysis ; test generation |
UDC | 004.45 |
Document type | Scientific report |
File type | Other |
Language | Russian |
Level of education | Graduate student |
Speciality code (FGOS) | 09.06.01 |
Speciality group (FGOS) | 090000 - Информатика и вычислительная техника |
Rights | Текст не доступен в соответствии с распоряжением СПбПУ от 11.04.2018 № 141 |
Additionally | New arrival |
Record key | ru\spstu\vkr\39364 |
Record create date | 9/29/2025 |
В работе представлен подход к повышению эффективности статического анализа программного обеспечения через моделирование поведения внешних библиотек с использованием формальных спецификаций, что позволяет упростить анализ многокомпонентных проектов и сократить время его выполнения. Работа включает обзор существующих методов, описание архитектуры системы для подстановки аппроксимаций функций стандартной библиотеки на языке LibSL, а также результаты экспериментальной проверки предложенного подхода.
The paper presents an approach to improving the efficiency of static software analysis via behavior modeling of external libraries using formal specifications, which allows for simplifying the analysis of multi-component projects and reduces the time requirements. The paper includes a review of existing methods, a description of the system architecture for substituting approximations of standard library functions in LibSL, as well as the results of experimental validation of the proposed approach.