Пошук академічних текстів

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