Институт системного программирования им. В.П. Иванникова РАН


О применении антиунификации подстановок для проверки эквивалентности программ.

Авторы

Захаров В.А., Новикова Т.А.

Аннотация

Предложено решение одного варианта задачи унификации программ. Задача унификации программ возникает при решении многих проблем системного программирования, к числу которых относятся задачи реорганизации программ, деобфускации программ, выявления уязвимостей в программном коде и др. Она является обобщением широко известной задачи синтаксической унификации термов. Нами разработан новый алгоритм проверки логико-термальной эквивалентности программ, основанный на операции вычисления точной нижней грани в решетке конечных подстановок. Сложность этого алгоритма оценивается величиной $O(n^6)$ , где $n$ – суммарный размер анализируемых программ. На основе построенного алгоритма проверки логико-термальной эквивалентности программ был разработан алгоритм логико-термальной унификации программ, которая состоит в построении для двух заданных фрагментов программного кода таких процедур, которые представляют собой наиболее общие специализации этих двух фрагментов.

Издание

Материалы 16-й Международной конференции «Проблемы теоретической кибернетики», Нижний Новгород, 20-25 июня 2011, 2011, Нижегородский государственный университет, с. 340-343.

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

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

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