Розглянуто властивості, сучасні системи та методи верифікації формальних моделей. Описано основні теоретичні відомості про інсерційне моделювання. Висвітлено алгоритми перевірки виконуваності формул, прямого та зворотного предикатних трансформерів. Наведено алгоритм розділення формули на спеціалізації, абстрактний предикатний трансформер, який є інваріантним щодо структур даних дедуктивної системи. Створено алгоритм усунення інтерлівінгу у символьних інсерційних моделях, введено поняття необхідної та достатньої умов переставності операторів, у тому числі поняття статичної та динамічної переставності. Узагальнено алгоритм для перевірки досяжності деяких станів користувача. Запропоновано алгоритм конкретизації символьних трас, який дозволяє отримувати конкретну трасу, що покривається висхідною символьною трасою. Висвітлено алгоритми змішаних обчислень для інсерційних моделей. Доведено існування оберненої поведінки у повній збагаченій алгебрі поведінки. Удосконалено мову REM, за допомогою вдосконалення якої доведено ефективність за часом недетермінованої стратегії переписування. Одержано ефективний алгоритм трансляції коду мовою APLAN до мови C++. Стисло описано систему VRS як комерційну систему, у якій використано основні результати дослідження. Представлено систему доказового програмування та елементи констрейтного програмування засобами інсерційного моделювання.

• Песчаненко Володимир Сергійович (фізико-математичні науки)

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"