Реєстраційний номер
0217U006013,
0116U004732
, Науково-дослідна робота
Назва роботи
Методи комп'ютерної алгебри та інсерційного моделювання в системах статичного аналізу та верифікації програмного забезпечення
Назва етапу роботи
Керівник роботи
Львов Михайло Сергійович,
Дата реєстрації
25-01-2017
Організація виконавець
Херсонський державний університет
Опис етапу
Проведено дослідження існуючих спеціалізованих систем статичного аналізу програм. Проведено аналіз алгоритмів комп'ютерної алгебри та інсерційного моделювання в системах статичного аналізу та верифікації програмного забезпечення. Розглянуто новий метод доведення інваріантності системи лінійних нерівностей, а також завершуваності лінійно визначених ітеративних циклів для імперативних програм.Розглянуто алгоритм побудови канонічних форм логічних формул над типами даних. Визначено функціональні вимоги та спроектовано структуру Web-ресурсу предметної області та наукової групи в цілях міжнародного наукового співробітництва.Сформовано зміст бібліотеки алгоритмів комп'ютерної алгебри статичного аналізу програм. Визначено функціональні вимоги та спроектовано структуру Web-ресурсу бібліотеки алгоритмів комп'ютерної алгебри статичного аналізу програм.
Опис продукції
Метод доведення інваріантності системи лінійних нерівностей, а також завершуваності лінійно визначених ітеративних циклів для імперативних програм. . Алгоритм побудови канонічних форм логічних формул над типами даних. Функціональні вимоги та структура Web-ресурсу предметної області та наукової групи в цілях міжнародного наукового співробітництва та Web-ресурсу бібліотеки алгоритмів комп'ютерної алгебри статичного аналізу програм.
Автори роботи
Блинов І.О.
Вінник М.О.
Кльонов Д.М.
Кушнір Н.О.
Мельник Д.Г.
Нємченко Д.О.
Надєєва В.В.
Песчаненко В.С.
Полторацький М.Ю.
Приймак К.С.
Тарасіч Ю.Г.
Черненко І.Є.
Шорнік В.М.
Додано/оновлено в НРАТ
2020-04-02
