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