Проблема эквивалентности программ: модели, алгоритмы, сложность тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

Защита состоится 02 марта 2012 г. в 11.00 на заседании диссертационного совета Д 501.001.44 при Московском государственном университете имени М.В. Ломоносова по адресу 119991, ГСП-1, Москва, Ленинские горы, МГУ, 2-й учебный корпус, факультет ВМК, ауд. 685.

С диссертацией можно ознакомиться в библиотеке факультета ВМК МГУ Автореферат разослан 29 ноября 2011 г.

Ученый секретарь диссертационного совета профессор

Общая характеристика диссертационной работы

Тема исследований диссертационной работы — проблема эквивалентности программ. Исследования охватывают несколько аспектов этой проблемы: математические модели программ, используемые для ее формализации, отношения между этими моделями, методы построения разрешающих алгоритмов в некоторых моделях программ, сложность проблемы эквивалентности.

Проблема эквивалентности программ состоит в том, чтобы для произвольной заданной пары программ выяснить, имеют ли эти программы одинаковое поведение. Строгие определения терминов «программа» и «поведение», фигурирующих в этой формулировке, могут варьироваться, и поэтому проблема эквивалентности программ охватывает целый спектр задач проверки схожести разных видов поведения программ в различных моделях вычислений.

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

Проблема эквивалентности имеет важное эпистемологическое значение. Понимание смысла объектов некоторого класса проявляется, в частности, в способности распознавать, имеют ли два объекта одинаковый смысл. Смысл программы определяется ее вычислениями. Поэтому, изучая методы решения и сложность проблемы эквивалентности, мы тем самым оцениваем уровень математических средств и объем вычислительных ресурсов, которые потребуются для решения других задач семантического анализа программ. Формально это объясняется тем, что большое число задач анализа программ может быть сведено к проблеме эквивалентности программ.

С проблемой эквивалентности программ сталкиваются при решении ряда задач системного программирования и компьютерной безопасности; к их

числу относятся задачи оптимизации, верификации, реорганизации и обфус-кации программ, задача обнаружения вредоносных программ (вирусов) и др.

Принципиальная трудность задач семантического анализа программ объясняется тем, что в любой «естественной» универсальной системе программирования любое нетривиальное функциональное свойство программ нерекурсивно (теорема Райса-Успенского). Этот факт не отменяет возможности получения эффективно проверяемых достаточных условий функциональной эквивалентности программ, однако, ни одно из этих достаточных условий не будет необходимым. Систематический подход к поиску эффективно проверяемых достаточных условий эквивалентности программ и построению систем эквивалентных преобразований был предложен и развит в работах A.A. Ляпунова, Ю.И. Янова, А.П. Ершова, В.М. Глушкова, A.A. Летичевского, Р.И. Подловченко, В.К. Сабельфельда, М.С. Патерсона, 3. Манны, Ш. Грейбах, Р. Милнера. Эти работы привели к созданию и развитию теории схем программ, в рамках которой сформировалась общая методика построения и применения моделей программ для решения проблем эквивалентности и эквивалентных преобразований. Основные положения этой методики таковы.

1). Формируется параметризованная модель вычислений, представляющая собой семейство моделей программ М(а). Объекты каждой модели обычно называются схемами программ. Параметр а определяет семантику базовых компонентов схем программ в модели М