Алгоритмы антиунификации и их применение для вычисления инвариантов программ (кандидатская диссертация)

Р. Э. Яворский (Отзыв ведущей организации)
Инвариант программы – отношение между данными, которое выполныется для любых вычислений программы. Знание инвариантов необходимо для решения практических задач верификации, оптимизации, синтеза и реорганизации (рефакторинга) программ. Задача антиунификации состоит в том, чтобы для двух заданных выражений $E_1$ и $E_2$ найти наиболее специальное выражение $E_0$, примерами которого являются оба выражения $E_1$ и $E_2$, т.е. существуют подстановки $T_1$ и $T_2$, для которых $E_1=E_0T_1$ и $E_2=E_0T_2$. Алгоритмы антиунификации могут использоваться для вычисления инвариантов программ.