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.