Оновлено: 05.05.2021

МЕТОДИ КОМП'ЮТЕРНОЇ АЛГЕБРИ ТА ІНСЕРЦІЙНОГО МОДЕЛЮВАННЯ В СИСТЕМАХ СТАТИЧНОГО АНАЛІЗУ ТА ВЕРИФІКАЦІЇ ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ

Керівник дослідженняЛьвов Михайло Сергійович

Номер державної реєстрації: 0116U004732

Номер облікової картки заключного звіту:0219U000269

Строки виконання: початок – 01.02.2016, закінчення – 31.12.2016

Обсяг коштів, виділених на виконання дослідження за весь період (згідно із запитом / фактичний) 900 / 620,775 тис. гривень

Предмет дослідження – Спеціалізована програмна система верифікації формальних моделей програм.

Об'єкт дослідження – Спеціалізовані програмні системи статичного аналізу та верифікації програмного забезпечення обчислювальних систем

Мета науково-дослідної роботи – створення загальної моделі спеціалізованої програмної системи статичного аналізу програм.

Основні завдання, задачі чи проблеми, які необхідно було вирішити для досягнення мети:

-      Розробка інсерційної моделі спеціалізованої програмної системи статичного аналізу програм;

-      Розробка інсерційної моделі системи генерації та перетворень різних типів математичних моделей об’єктних програм;

-      Розробка бібліотеки спеціальних алгоритмів комп’ютерної алгебри генерації та доведення програмних інваріантів та на її базі математичного ядра системи статичного аналізу програм.

-      Створення спеціального Web-ресурсу проекту, орієнтованого на міжнародне наукове співтовариство, з метою оприлюднення його результатів.