Реєстраційний номер
0821U102116, Дисертація доктора філософії
На здобуття
Доктор філософії
Дата захисту
30-06-2021
Статус
Захищена
Назва роботи
Статичний аналіз лінійно визначених програм і його застосування
Здобувач
Тарасіч Юлія Геннадіївна,
Керівник Львов Михайло Сергійович
Опонент Нікітченко Микола Степанович
Опонент Кирийчук Дмитро Леонідович
Рецензент Бабічев Сергій Анатолійович
Рецензент Вейцбліт Олександр Йосипович
Установа, організація, у вченій раді якої відбудеться/відбувся захист
Херсонський державний університет
Опис
Мета роботи полягає в аналізі існуючих алгоритмів комп’ютерної алгебри та інсерційного моделювання в системах статичного аналізу та верифікації програмного забезпечення, побудові ефективних алгоритмів статичного аналізу програм.
У розділі 1 надано аналіз існуючих методів та систем статичного аналізу, приведено базисні дефініції дисертаційного дослідження.
У розділі 2 розглянуто проблему генерації інваріантів програм, представлено нові методи доказу інваріантності системи лінійних нерівностей і завершуваності лінійно визначених ітеративних циклів імперативних програм.
У розділі 3 представлено новий алгоритм побудови канонічної форми лінійних півалгебраїчних формул (ЛПФ) та його реалізацію.
Практичне значення наукових результатів полягає в можливості застосування отриманих результатів у задачах верифікації програмного забезпечення, а саме – в розробці спеціалізованих програмних систем верифікації формальних моделей програм.
Дата реєстрації
2021-07-12
Додано/оновлено в НРАТ
2021-07-12 / 2026-07-01
