О применении антиунификации подстановок для проверки эквивалентности программ.
О применении антиунификации подстановок для проверки эквивалентности программ.
Авторы
Аннотация
Предложено решение одного варианта задачи унификации программ. Задача унификации программ возникает при решении многих проблем системного программирования, к числу которых относятся задачи реорганизации программ, деобфускации программ, выявления уязвимостей в программном коде и др. Она является обобщением широко известной задачи синтаксической унификации термов. Нами разработан новый алгоритм проверки логико-термальной эквивалентности программ, основанный на операции вычисления точной нижней грани в решетке конечных подстановок. Сложность этого алгоритма оценивается величиной $O(n^6)$ , где $n$ – суммарный размер анализируемых программ. На основе построенного алгоритма проверки логико-термальной эквивалентности программ был разработан алгоритм логико-термальной унификации программ, которая состоит в построении для двух заданных фрагментов программного кода таких процедур, которые представляют собой наиболее общие специализации этих двух фрагментов.
Издание
Материалы 16-й Международной конференции «Проблемы теоретической кибернетики», Нижний Новгород, 20-25 июня 2011, 2011, Нижегородский государственный университет, с. 340-343.
Научная группа
Все публикации за 2011 год
Все публикации