Оновлено: 05.05.2021
МЕТОДИ КОМП'ЮТЕРНОЇ АЛГЕБРИ ТА ІНСЕРЦІЙНОГО МОДЕЛЮВАННЯ В СИСТЕМАХ СТАТИЧНОГО АНАЛІЗУ ТА ВЕРИФІКАЦІЇ ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ
Керівник дослідження: Львов Михайло Сергійович
Номер державної реєстрації: 0116U004732
Номер облікової картки заключного звіту:0219U000269
Строки виконання: початок – 01.02.2016, закінчення – 31.12.2016
Обсяг коштів, виділених на виконання дослідження за весь період (згідно із запитом / фактичний) 900 / 620,775 тис. гривень
Предмет дослідження – Спеціалізована програмна система верифікації формальних моделей програм.
Об'єкт дослідження – Спеціалізовані програмні системи статичного аналізу та верифікації програмного забезпечення обчислювальних систем
Мета науково-дослідної роботи – створення загальної моделі спеціалізованої програмної системи статичного аналізу програм.
Основні завдання, задачі чи проблеми, які необхідно було вирішити для досягнення мети:
- Розробка інсерційної моделі спеціалізованої програмної системи статичного аналізу програм;
- Розробка інсерційної моделі системи генерації та перетворень різних типів математичних моделей об’єктних програм;
- Розробка бібліотеки спеціальних алгоритмів комп’ютерної алгебри генерації та доведення програмних інваріантів та на її базі математичного ядра системи статичного аналізу програм.
- Створення спеціального Web-ресурсу проекту, орієнтованого на міжнародне наукове співтовариство, з метою оприлюднення його результатів.