Быстрые алгоритмы антиунификации и их применение при анализе программ.

Авторы

Захаров В.А., Костылев Е.В.

Аннотация

Исследована задача антиунификации логических выражений. Эта задача заключается в построении для заданного множества выражений такого наименее общего выражения (шаблона), примерами которого являются все выражения исходного множества. Для случая, когда выражения имеют вид формул, предложены два алгоритма построения наиболее специальных шаблонов. Один из этих алгоритмов использует теоретико-графовое представление формул и имеет вычислительную сложность, близкую к линейной. Показано, что предложенные алгоритмы могут применяться при решении задач верификации и статического анализа программ.

Ключевые слова

анализ программ, инвариант, антиунификация

Издание

Материалы XIII Международной школы-семинара «Синтез и сложность управляющих систем", 2002, Пенза, с. 76-81.

Научная группа

Теоретическая информатика

Все публикации за 2002 год

Все публикации