Тарасіч Ю. Г. Статичний аналіз лінійно визначених програм і його застосування

Мета роботи полягає в аналізі існуючих алгоритмів комп’ютерної алгебри та інсерційного моделювання в системах статичного аналізу та верифікації програмного забезпечення, побудові ефективних алгоритмів статичного аналізу програм. У розділі 1 надано аналіз існуючих методів та систем статичного аналізу, приведено базисні дефініції дисертаційного дослідження. У розділі 2 розглянуто проблему генерації інваріантів програм, представлено нові методи доказу інваріантності системи лінійних нерівностей і завершуваності лінійно визначених ітеративних циклів імперативних програм. У розділі 3 представлено новий алгоритм побудови канонічної форми лінійних півалгебраїчних формул (ЛПФ) та його реалізацію. Практичне значення наукових результатів полягає в можливості застосування отриманих результатів у задачах верифікації програмного забезпечення, а саме – в розробці спеціалізованих програмних систем верифікації формальних моделей програм.