Захаров Владимир Анатольевич

Захаров Владимир Анатольевич

Захаров Владимир Анатольевич — доктор физико-математических наук, профессор.

Области научных интересов

Задача проверки эквивалентности программ

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

Обфускация программ

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

Верификация моделей программ

Задача верификации моделей программ (model checking) состоит в том, чтобы для заданной модели программ, представленной системой переходов, выражением алгебры процессов, автоматом и пр., и спецификации программы, представленной формулой темпоральной логики, требуется проверки выполнимость спецификации на модели. В этом случае удается математически строго доказать, что проверяемая программа работает правильно.

Логическое программирование

Разрабатываются и исследуются методы анализа логических программ.

Статический анализ программ

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

Модели параллельных вычислений

Конструируются и исследуются математические модели параллельных вычислений. Разрабатываются математические методы анализа моделей параллельных вычислений.

Программно конфигурируемые сети

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

Лекционные курсы

• Математическая логика и логическое программирование (3-й поток)
• Математическая логика и логическое программирование (318 группа)
• Модели вычислений
• Математическая логика и теория алгоритмов
• Распределенные алгоритмы

Спецсеминары

• Теоретические проблемы программирования ‎
• Некоторые вопросы теории управляющих систем

Аспиранты и студенты

1. Подымов Владислав Васильевич
2. Новикова Татьяна Анатольевна
3. Попеско Ульна Владиславовна

Избранные публикации

Статьи в журналах

2014 Двусторонняя унификация программ и ее применение для задач рефакторинга

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

в журнале Труды Института системного программирования РАН (электронный журнал), том 26, № 2, с. 245-268

2013 Формальная модель и задачи верификации программно-конфигурируемых сетей Захаров В.А., Смелянский Р.Л., Чемерицкий Е.В. в журнале Моделирование и анализ информационных систем, том 20, № 6, с. 33-48

 2012  Как разработать простое средство верификации систем реального времени 

Волканов Д.Ю., Захаров В.А., Зорин Д.А., Коннов И.В., Подымов В.В. в журнале Моделирование и анализ информационных систем, том 19, № 6, с. 45-56

 2012  О разработке средств верификации для распределенных вычислительных систем реального времени 

Волканов Д.Ю., Захаров В.А., Зорин Д.А., Коннов И.В., Подымов В.В. в журнале Моделирование и анализ информационных систем, том 19, № 5

 2012  Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ 

Захаров В.А., Новикова Т.А. в журнале Труды Института системного программирования РАН (электронный журнал), том 22, с. 435-455

 2012  Унификация программ 

Новикова Т.А., Захаров В.А. в журнале Труды Института системного программирования РАН (электронный журнал), том 23, с. 455-476

 2011  Применение алгебры подстановок для унификации программ 

Захаров В.А., Новикова Т.А. в журнале Труды Института системного программирования РАН (электронный журнал), том 21, с. 141-166

 2010  An invariant-based approach to the verification of asynchronous parameterized networks 

Konnov I.V., Zakharov V.A. в журнале Journal of Symbolic Computation, издательство Academic Press (United States), том 45, № 11, с. 1144-1162

 2010  Program equivalence checking by two-tape automata 

Zakharov V.A. в журнале Cybernetics and Systems Analysis, издательство Kluwer Academic Publishers (Netherlands), том 46, № 4, с. 554-562

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

Захаров В.А., Коннов И.В. в журнале Моделирование и анализ информационных систем, том 17, № 4, с. 78-87

 2010  Об одной полугрупповой модели программ, определяемой при помощи двухленточных автоматов 

Захаров В.А., Подымов В.В. в журнале Научные ведомости Белгородского государственного университета. Серия История, экономика, политология, информатика, том 14, № 7, с. 94-101

 2010  Проверка эквивалентности программ при помощи двухленточных автоматов 

Захаров В.А. в журнале Кибернетика и системный анализ, № 4, с. 39-48

 2009  Использование алгебраических моделей программ для обнаружения метаморфного вредоносного кода 

Захаров В.А., Кузюрин Н.Н., Подловченко Р.И., Щербина В.Л. в журнале Фундаментальная и прикладная математика, том 15, № 5, с. 181-198

 2009  О верификации конечных параметризованных моделей распределенных программ 

Захаров В.А., Булычев П.Е. в журнале Научные ведомости Белгородского государственного университета. Серия История, экономика, политология, информатика, том 9, № 11, с. 116-123

 2009  О стойкой обфускации компьютерных программ 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В. в журнале Научные ведомости Белгородского государственного университета. Серия История, экономика, политология, информатика, том 15, № 12, с. 97-105

 2008  О сложности задачи антиунификации 

Захаров В.А., Костылев Е.В. в журнале Дискретная математика, том 20, № 1, с. 131-144

 2008  Эффективные алгоритмы проверки эквивалентности программ в моделях, связанных с обработкой прерываний 

Захаров В.А., Щербина В.Л. в журнале Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика, № 2, с. 33-41

 2007  Применение методов теории игр к поиску некоторых видов симуляции на размеченных системах переходов с ограничениями справедливости 

Булычев П.Е., Захаров В.А. в журнале Вестник МЭИ, № 6, с. 5-9

 2007  Современные методы обфускации программ: классификация и сравнительный анализ 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В. в журнале Известия Южного федерального университета. Технические науки, том 76, № 1, с. 93-99

 2006  О применении методов деобфускации программ для обнаружения сложных компьютерных вирусов 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Подловченко Р.И., Шокуров А.В., Щербина В.Л. в журнале Известия Южного федерального университета. Технические науки, том 2, № 7, с. 18-27

 2005  Методы защиты проектных решений при проектировании микроэлектронных схем 

Варновский Н.П., Захаров В.А., Иванников В.П., Кузюрин Н.Н., Шокуров А.В., Кононов А.Н., Калинин А.В. в журнале Известия ТРТУ, № 4, с. 112-119

 2005  Об одном обобщении подстановки применительно к задаче статического анализа программ 

Захаров В.А., Костылев Е.В. в журнале Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика, том 4, с. 39-45

 2005  Об одном подходе к верификации симметрических параметризованных распределенных систем 

Захаров В.А., Коннов И.В. в журнале Программирование, № 5, с. 24-36

 1999  On the decidability of the equivalence problem for orthogonal sequential programs 

Zakharov V.A. в журнале Grammars, том 2, № 3, с. 271-281 DOI

 1999  Быстрые алгоритмы разрешения эквивалентности пропозициональных операторных программ на упорядоченных полугрупповых шкалах 

Захаров В.А. в журнале Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика, № 3, с. 29-35

 1998  Аппроксимация абстрактных семантик формальными моделями программ 

Захаров В.А. в журнале Дискретная математика, том 10, № 4, с. 119-141

 1998  О восстановлении сети процесса по последовательности срабатываний переходов сети Петри 

Захаров В.А., Тхуан Н.Н., Бан Д.В., Хынг Д.В. в журнале Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика, № 2, с. 31-34

 1998  Полиномиальный по сложности алгоритм, распознающий коммутативную эквивалентность схем программ 

Захаров В.А., Подловченко Р.И. в журнале Доклады Российской Академии наук, том 362, № 6, с. 744-747

 1998  Эффективные алгоритмы проверки выполнимости формул темпоральной логики CTL на модели и их применение для верификации параллельных программ 

Захаров В.А., Царьков Д.В. в журнале Программирование, № 4, с. 43-47

 1997  О взаимосвязи двух семантик параллельных вычислений 

Захаров В.А., Спанопуло В.В. в журнале Программирование, № 4, с. 36-48

 1994  О преобразовании операторных процедур в логические программы 

Захаров В.А., Маневич С.И. в журнале Программирование, № 6, с. 23-39

 1994  Об отношении аппроксимируемости семантик операторных программ 

Захаров В.А. в журнале Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика, № 3, с. 54-60

 1994  Условия сглаживаемости операторных формальных моделей программ 

Захаров В.А. в журнале Программирование, № 5, с. 23-40

 1993  Об одном критерии сравнимости операторных формальных моделей программ 

Захаров В.А. в журнале Программирование, № 4, с. 12-25

 1992  Формальные модели программ и свободные схемы 

Захаров В.А. в журнале Программирование, № 2, с. 10-24

 1989  Об автоматных схемах программ 

Захаров В.А. в журнале Доклады Академии наук СССР, том 309, № 1, с. 24-27

 1986  Автоматные модели машин Тьюринга 

Захаров В.А. в журнале Доклады Академии наук СССР, том 291, № 2, с. 280-284

Статьи в сборниках

2014  On the NetworkUpdate Problem for Software Defined Networks 

Chemeritskii E.V., Zakharov V.A. в сборнике Proceedings of the 5-th Workshop "Program Semantics, Specification and Verification: Theory and Applications", Moscow, Russia, June 4, 2014, место издания Москва, с. 26-37

 2014  Two-sided unification is NP-complete 

Tatyana Novikova, Vladimir Zakharov в сборнике Proceedings of the 28-th International Workshop on Unification (UNIF-2014), серия RISC-Linz Report Series, место издания Research Institute for Symbolic Computation, Johanes Kepler University Linz, Austria, том 6, с. 55-61

 2014  О сложности задачи решения линейных уравнений над конечными подстановками 

Новикова Т.А., Захаров В.А. в сборнике Материалы XVII Международной конференции "Проблемы теоретической кибернетики" (Казань, 16-20 июня 2014 г.), место издания Казань: Отечество Казань, с. 221-223

 2014  Об эквивалентности ограниченно недетерминированных автоматов-преобразователей над полугруппами 

Захаров В.А. в сборнике Материалы XVII Международной конференции "Проблемы теоретической кибернетики" (Казань, 16-20 июня 2014 г.), место издания Казань: Отечество Казань, с. 100-102

 2013  A Formal Model and Verification Problems for Software Defined Networks 

Chemeritsky E.V., Smelyansky R.L., Zakharov V.A. в сборнике Proceedings of the 4-th International Workshop "Program Semantics, Specification and Verification: Theory and Applications", место издания Yekaterinburg, Russia, с. 21-30

 2013  An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts 

Konnov I.V., Podymov V.V., Volkanov D.Yu, Zakharov V.A., Zorin D.A. в сборнике Proceedings of the International Workshop on Verification of Embedded Systems 2013 (VES 2013). Saint, место издания Saint Petersburg State Polytechnical University Petersburg, Russia, с. 32-46

 2013  DYANA: an integrated development environment for simulation and verification of real-time avionics systems 

Antonenko V.A., Chemeritsky E.V., Glonina A.B., Konnov I.V., Pashkov V.N., Podymov V.V., Savenkov K.O., Smeliansky R.L., Vdovin P.M., Volkanov D.Yu, Zakharov V.A., Zorin D.A. в сборнике Proc. of the 5th EUCASS conference for aerospace science (EUCASS 2013), место издания Munich. Germany

 2013  Is it possible to unify sequential programs 

Novikova T.A., Zakharov V.A. в сборнике Proceedings of the 27-th International Workshop on Unification, June 26, 2013, Eindhoven, серия EPiC Series, том 123, с. 36-46

 2013  Методика использования системы имитационного моделирования РВС РВ ДИАНА, основанной на стандарте HLA 

Волканов Д.Ю., Антоненко В.А., Герасёв А.В., Глонина А.Б., Захаров В.А., Зорин Д.А., Коннов И.В., Пашков В.Н., Подымов В.В., Савенков К.О., Смелянский Р.Л., Чемерицкий Е.В. в сборнике Сборник докладов шестой всероссийской научно-практической конференции "Имитационное моделирование. Теория и практика" (ИММОД-2013), место издания Издательство "ФЭН" Академии наук РТ, Казань, том 1, с. 322-326

 2012  On the Designing of Model Checkers for Real-Time Distributed Systems 

Konnov I.V., Podymov V.V., Volkanov D.Yu, Zorin D.A., Zakharov V.A. в сборнике 3-rd Workshop “Program Semantics, Specification, and Verification: Theory and Applications”, Nizhni Novgorod, Russia, July 1-2, 2012, место издания Novgorod, Russia, с. 72-81

 2012  Методика использования системы имитационного моделирования РВС РВ, базирующейся на стандарте HLA 

Антоненко В.А., Вдовин П.М., Волканов Д.Ю., Глонина А.Б., Захаров В.А., Зорин Д.А., Коннов И.В., Пашков В.Н., Подымов В.В., Савенков К.О., Смелянский Р.Л., Чемерицкий Е.В. в сборнике Программные системы и инструменты. Тематическкий сборник, место издания Изд. отделения ф-та ВМК МГУ Москва, том 12, с. 105-116

 2012  Модели и алгоритмы в задаче проверки эквивалентности программ 

Захаров В.А. в сборнике Материалы XI Международного семинара «Дискретная математика и ее приложения», посвященного 80-летию со дня рождения академика О.Б. Лупанова (Москва, МГУ, 18-23 июня 2012 г.), место издания Изд-во механико-математического ф-та МГУ Москва, с. 53-62

 2012  О логико-термальной эквивалентности стандартных схем программ 

Захаров В.А., Новикова Т.А. в сборнике Материалы XI Международного семинара «Дискретная математика и ее приложения», посвященного 80-летию со дня рождения академика О.Б. Лупанова (Москва, МГУ, 18-23 июня 2012 г.), место издания Изд-во механико-математического ф-та МГУ Москва, с. 147-149

 2012  Об эквивалентности металинейных унарных рекурсивных программ 

Захаров В.А., Подымов В.В. в сборнике Материалы XI Международного семинара «Дискретная математика и ее приложения», посвященного 80-летию со дня рождения академика О.Б. Лупанова (Москва, МГУ, 18-23 июня 2012 г.), место издания Изд-во механико-математического ф-та МГУ Москва, с. 157-159

 2012  Об эквивалентности потоковых программ 

Захаров В.А. в сборнике Материалы XI Международного семинара «Дискретная математика и ее приложения», посвященного 80-летию со дня рождения академика О.Б. Лупанова (Москва, МГУ, 18-23 июня 2012 г.), место издания Изд-во механико-математического ф-та МГУ Москва, с. 119-121

 2011  Методика использования системы имитационного моделирования РВС РВ, базирующейся на стандарте HLA 

Антоненко В.А., Вдовин П.М., Волканов Д.Ю., Глонина А.Б., Захаров В.А., Зорин Д.А., Коннов И.В., Пашков В.Н., Подымов В.В., Савенков К.О., Смелянский Р.Л., Чемерицкий в сборнике Программные системы и инструменты. Тематический сборник, место издания факультета ВМиК МГУ Москва, том 13, с. 105-116

 2011  О двухленточных машинах, описывающих полугруппы с сокращением 

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

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

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

 2011  О проблеме эквивалентности потоковых программ 

Захаров В.А. в сборнике Труды Второй Международной научно-технической конференции «Компьютерные методы и технологии», Белгород, 3-6 октября 2011, место издания Белгородский государственный университет Белгород, с. 34-37

 2010  Using adaptive symmetry reduction for LTL model checking 

Konnov I.V., Zakharov V.A. в сборнике Труды семинара «Семантика, спецификация и верификация программ: теория и приложения». Казань, 14-15 июня 2010, с. 5-11

 2010  Языки описания схем. Проблемы верификации 

Корухова Ю.С., Захаров В.А. в сборнике Программы специальных курсов факультета ВМК МГУ / Ред. Березин Б.И,, Ломов И.С. Сост. Кобелева А.Н, место издания МАКС Пресс Москва МГУ, с. 188-190

 2009  Anti-unification algorithms and their applications in program analysis 

Bulychev P.E., Kostylev E.V., Zakharov V.A. в сборнике Proceedings of the 7th International Conference “Perspectives of System Informatics”, June 15-19, 2009, Novosibirsk, серия Lecture Notes in Computer Science, место издания Springer, том 5947, с. 413-424

 2009  Anti-unification algorithms and their applications in program analysis 

Bulychev P.E., Kostylev E.V., Zakharov V.A. в сборнике Pre-Proceedings of the 7th International Conference “Perspectives of System Informatics”, June 15-19, 2009, Novosibirsk, место издания Novosibirsk, с. 82-89

 2009  Establishing Linux Driver Verification Processes 

Khoroshilov A., Petrenko A., Mutilin V., Zakharov V.A. в сборнике Proceedings of the 7th International Conference “Perspectives of System Informatics”, June 15-19, 2009, Novosibirsk, серия Lecture Notes in Computer Science, место издания Springer, том 5947, с. 165-176

 2009  Establishing Linux Driver Verification Processes 

Khoroshilov A., Mutilin V., Petrenko A.K., Zakharov V.A. в сборнике Pre-Proceedings of the 7th International Conference “Perspectives of System Informatics”, June 15-19, 2009, Novosibirsk, место издания Novosibirsk, с. 124-131

 2009  Two-tape machinery for the equivalence checking of sequential programs 

Zakharov V.A. в сборнике Proceedings of the International Workshop on Program Understanding, June 20-22, 2009, Novosibirsk, место издания Novosibirsk, с. 28-40

 2009  Возможна ли стойкая обфускация программ 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В. в сборнике Труды Первой Международной научно-технической конференции «Компьютерные методы и технологии», Белгород, 8-10 октября, 2009, с. 25-29, место издания Белгород, с. 25-29

 2009  Об одной задаче верификации параметризованных конечных систем переходов 

Булычев П.Е., Захаров В.А. в сборнике Труды Третьей Всероссийской конференции «Методы и средства обработки информации», Москва, 2009, место издания Москва, с. 98-104

 2009  Об одном обобщении подстановки применительно к вычислению инвариантов программ 

Захаров В.А., Костылев Е.В. в сборнике Труды Третьей Всероссийской конференции «Методы и средства обработки информации», Москва, 2009, место издания Москва, с. 123-130

 2009  Универсальный подход к проверке отношений симуляции для моделей программ 

Булычев П.Е., Захаров В.А. в сборнике Труды Третьей Всероссийской конференции «Методы и средства обработки информации», Москва, 2009, место издания Москва, с. 104-110

 2008  How to cook an automated system for Linux driver verification 

Khoroshilov A., Mutilin V., Shcherbina V., Strikov O., Vinogradov S., Zakharov V.A. в сборнике Proceedings of the 1st Spring Young Researchers’ Colloquium on Software Engineering SYRCoSE 2008 (St Petersburg, May 29-30, 2008), место издания Санкт-Петербург, с. 15-19

 2007  An invariant-based approach to the verification of asynchronous parameterized networks 

Konnov I.V., Zakharov V.A. в сборнике Proceedings of the 1-st International Workshop on Invariant Generation, June 25-26, 2007, Hagenberg, Austria, место издания Hagenberg, Austria, с. 41-55

 2007  Computing (bi)simulation relations preserving CTL-X- logic for ordinary and fair Kripke structures 

Bulychev P.E., Konnov I.V., Zakharov V.A. в сборнике Труды Института Системного программирования, место издания ИСП РАН Москва, том 12, с. 59-76

 2007  On the concept of software obfuscation in computer security 

Kuzurin N.N., Shokurov A.V., Varnovskij N.P., Zakharov V.A. в сборнике Proceedings of the 7-th Information Security Conference (ISC'07), Valparaiso, Chile, серия Lecture Notes in Computer Science, место издания Springer Berlin, том 4779, с. 281-298

 2007  On the verification of asynchronous parameterized networks of communicating processes by model checking 

Konnov I.V., Zakharov V.A. в сборнике Труды Института Системного программирования, место издания ИСП РАН Москва, том 12, с. 37-58

 2007  Using algebraic models of programs for detecting metamorphic malwares 

Kuzurin N.N., Podlovсhenko R.I., Shcherbina V.L., Zakharov V.A. в сборнике Труды Института Системного программирования, место издания ИСП РАН Москва, том 12, с. 77-94

 2006  Encoding mobile ambients into pi-calculus 

Ciobanu G., Zakharov V.A. в сборнике Pre-Proceedings of the Andrei Ershov 6th International Conference «Prespectives of System Informatics» (27-30 June 2006, Novosibirsk), место издания Novosibirsk, с. 79-91

 2006  Encoding mobile ambients into the pi-calculus 

Ciobanu G., Zakharov V.A. в сборнике Proceedings of the Andrei Ershov 6th International Conference «Prespectives of System Informatics» (27-30 June 2006, Novosibirsk), серия Lecture Notes in Computer Science, место издания Springer Berlin, том 4378, с. 148-161

 2006  On the equivalence problem for programs with mode switching 

Podlovchenko R.I., Rusakov D.M., Zakharov V.A. в сборнике Proceedings of CIAA-2005 "The 10-th International Conference on Implementation and Application of Automata" (June 27-29, 2005), Sophia Antipolis, France, серия Lecture Notes in Computer Science, место издания Springer, том 3845, с. 351-352

 2006  The equivalence problem for programs with mode switching is PSPACE-complete 

Podlovchenko R.I., Rusakov D.M., Zakharov V.A. в сборнике Труды Института Системного программирования, место издания ИСП РАН, том 11, с. 111-135

 2006  К вопросу об обфускации конечных автоматов 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В. в сборнике Материалы IX международной конференции «Интеллектуальные системы и компьютерные науки» (23-27 октября 2006 г.), место издания Изд-во механико-математического ф-та МГУ Москва, том 1, с. 127-130

 2006  О проблеме логико-термальной эквивалентности последовательных программ с динамической памятью 

Захаров В.А., Иванов К.С. в сборнике Труды Института Системного программирования, место издания ИСП РАН, том 11, с. 61-82

 2006  О проблеме обфускации программ 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В. в сборнике Материалы зимних научных чтений факультета социологии и информационных технологий и XIII социологических чтений Российского государственного социального университета (1-4 февраля 2006 года), место издания Изд-во Московского государственного социального университета Москва, с. 204-206

 2006  Об особенностях применения методов обфускации программ для информационной защиты микроэлектронных схем 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В., Чернов А.В. в сборнике Труды Института Системного программирования, место издания ИСП РАН, том 11, с. 29-60

 2005  On the equivalence checking problem for a model of programs related with muti-tape automata 

Zakharov V.A., Zakharyaschev I.M. в сборнике Proceedings of the 9-th International Conference on Implementation and Application of Automata (CIAA'04), July 22-24, 2004), Kingston, Ontario, Canada, серия Lecture Notes in Computer Science, место издания Springer, том 3317, с. 293-305

 2005  On the equivalence problem for programs with mode switching 

Podlovchenko R.I., Rusakov D.M., Zakharov V.A. в сборнике Pre-Proceedings of CIAA-2005 "The 10-th International Conference on Implementation and Application of Automata" (June 27-29, 2005), Sophia Antipolis, место издания France, с. 285-287

 2005  Математические проблемы обфускации 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н. в сборнике Математика и безопасность информационных технологий. Материалы конференции в МГУ 28-29 октября 2004 г., место издания МЦНМО, с. 65-91

 2005  О возможности применения быстрых алгоритмов проверки эквивалентности программ для обнаружения вирусов 

Захаров В.А., Захарьящев И.М., Подловченко Р.И., Русаков Д.М., Щербина В.Л. в сборнике Труды второй всероссийской конференции «Методы и средства обработки информации», место издания Изд-во ф-та ВМК МГУ Москва, с. 414-421

 2005  О формальной верификации криптографических протоколов с использованием spi-исчисления 

Захаров В.А., Корчевский А.А. в сборнике Труды второй всероссийской конференции «Методы и средства обработки информации», место издания Изд-во ф-та ВМК МГУ Москва, с. 373-379

 2005  Об одном подходе к верификации асинхронных параметризованных систем 

Захаров В.А., Коннов И.В. в сборнике Труды второй всероссийской конференции «Методы и средства обработки информации», место издания Изд-во ф-та ВМК МГУ Москва, с. 367-373

 2004  On the equivalence-checking problem for a model of programs related with multi-tape automata 

Zakharov V.A., Zakharyaschev I.M. в сборнике Pre-Proceedings of CIAA-2004 "The 9-th International Conference on Implementation and Application of Automata" (July 22-24, место издания Kingston, Ontario, Canada, с. 231-240

 2004  On the equivalence-checking problem for polysemantic models of sequential programs 

Zakharov V.A., Zakharyaschev I.M. в сборнике Труды Института Системного программирования, место издания ИСП РАН Москва, том 6, с. 182-199

 2004  Program obfuscation as obstruction of program static analysis 

Ivanov K.S., Zakharov V.A. в сборнике Труды Института Системного программирования, место издания ИСП РАН Москва, том 6, с. 141-161

 2004  Математические проблемы обфускации 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н. в сборнике Труды конференции "Математика и безопасность информационных технологий" (МаБИТ-04), Москва, 28-29 октября 2004 г, место издания Московский Центр Непрерывного Математического Образования, с. 54-72

 2004  О проблеме эквивалентности для программ с частично перестановочными и монотонными операторами 

Захаров В.А., Захарьящев И.М. в сборнике Труды 6-ой Международной конференции «Дискретные модели в теории управляющих систем", 7-11 декабря 2004 г., Москва, место издания МАКС Пресс - МГУ Москва, с. 105-109

 2004  О сложности проблемы эквивалентности в модели программ с перестановочными и монотонными операторами 

Захаров В.А., Захарьящев И.М. в сборнике Материалы VIII Международного семинара «Дискретная математика и ее приложения» (Москва, 2-6 февраля 2004 г.), место издания Изд-во механико-математического ф-та МГУ Москва, с. 131-134

 2004  Об одной алгебраической модели программ, связанной с обработкой прерываний 

Захаров В.А. в сборнике Материалы VIII Международного семинара «Дискретная математика и ее приложения» (Москва, 2-6 февраля 2004 г.), место издания Изд-во механико-математического ф-та МГУ Москва, с. 129-131

 2004  Об одной модели последовательных программ с динамической памятью 

Захаров В.А., Иванов К.С. в сборнике Труды 6-ой Международной конференции «Дискретные модели в теории управляющих систем", 7-11 декабря 2004 г., Москва, место издания МАКС Пресс - МГУ Москва, с. 112-116

 2004  Об одном обобщении подстановок применительно к задаче синтеза инвариантов программ 

Захаров В.А., Костылев Е.В. в сборнике Материалы VIII Международного семинара «Дискретная математика и ее приложения» (Москва, 2-6 февраля 2004 г.), место издания Изд-во механико-математического ф-та МГУ Москва, с. 134-137

 2003  An equivalence-checking algorithm for polysemantic models of sequential programs 

Zakharov V.A., Zakharyaschev I.M. в сборнике Proceedings of the International Workshop on Program Understanding (14-16 July, 2003, Altai Mountains), место издания Новосибирск, с. 59-70

 2003  On the possibility of provably secure obfuscating programs 

Varnovskij N.P., Zakharov V.A. в сборнике Proceedings of the Andrei Ershov 5th International Conference «Prespectives of System Informatics» (PSI'03) , 9-12 July 2003, Novosibirsk, серия Lecture Notes in Computer Science, место издания Springer, том 2890, с. 91-102

 2003  К вопросу о существовании стойких обфускаторов программ 

Варновский Н.П., Захаров В.А. в сборнике Труды V Международной конференции «Дискретные модели в теории управляющих систем», (Ратмино, 26-29 мая 2003 г.), место издания МАКС-Пресс - МГУ Москва, с. 26-29

 2003  О верификации параметризованных симметричных систем распределенных программ 

Захаров В.А., Коннов И.В. в сборнике Труды Первой Всероссийской научной конференции "Методы и средства обработки информации, место издания Издательский отдел факультета вычислительной математики и кибернетики МГУ им. М.В. Ломоносова Москва, с. 395-400

 2003  О перспективах решения задачи обфускации компьютерных программ 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В. в сборнике Труды конференции (МаБИТ-03) , Москва, 22-24 октября 2003 г, место издания Московский Центр Непрерывного Мватематического Образования Москва, с. 344-352

 2003  О противодействии некоторым алгоритмам статического анализа программ 

Захаров В.А., Иванов К.С. в сборнике Труды конференции "Математика и безопасность информационных технологий" (МаБИТ-03) , Москва, 22-24 октября 2003 г, место издания Московский Центр Непрерывного Математического Образования Москва, с. 282-287

 2003  Об одной полисемантической модели последовательных программ 

Захаров В.А., Захарьящев И.М. в сборнике Труды V Международной конференции «Дискретные модели в теории управляющих систем", (Ратмино, 26-29 мая 2003 г.), место издания МАКС Пресс-МГУ Москва, том 1, с. 26-29

 2003  Об одной системе вывода, связанной со статическим анализом программ 

Захаров В.А., Викторова М.С. в сборнике Труды V Международной конференции «Дискретные модели в теории управляющих систем», (Ратмино, 26-29 мая 2003 г.), место издания МАКС-Пресс - МГУ Москва, с. 26-29

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

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

 2001  An approach to the obfuscation of control-flow of sequential computer programs 

Chow S., Gu Y., Johnson H., Zakharov V.A. в сборнике Proceedings of the First "Information Security Conference", Malaga, Spain, 2001, серия Lecture Notes in Computer Science, том 2200, с. 144-155

 2001  The equivalence problem for computational models: Decidable and Undecidable Cases 

Zakharov V.A. в сборнике Proceedings of the Third International Conference, MCU 2001 Chişinau, Moldova, May 23–27, 2001, серия Lecture Notes in Computer Science, издательство SPRINGER HEIDELBERG (TIERGARTENSTRASSE 17, HEIDELBERG, GERMANY,D-69121), том 2055, с. 133-153

 2001  To the obfuscation of sequential program control-flow 

Zakharov V.A. в сборнике Труды XII Байкальской международной конференции, Иркутск, Байкал, 24-июня-1 июля, место издания Иркутский государственный университет Иркутск, том 5, с. 57-61

 2001  О проблеме эквивалентности операторных программ на одном классе уравновешенных шкал 

Захаров В.А. в сборнике Материалы VII Международного семинаpа «Дискpетная математика и ее пpиложения.», серия Часть II, место издания М.: МАКС Пресс,, с. 54-57

 2001  О проблеме эквивалентности операторных программ на уравновешенных однородных обратимых шкалах 

Захаров В.А. в сборнике Математические вопpосы кибеpнетики, место издания М.: Физматлит, том 10, с. 134-144

 2001  Теоретико-автоматный подход к определению формальных семантик языков программирования 

Захаров В.А., Кончаков Р.В. в сборнике , Труды Международной конференции "Параллельные вычисления и задачи управления" Москва, 2-4 октября 2001 г. Институт проблем управления им. В.А.Трапезникова РАН, место издания Изд-во Института проблем управления им. В.А.Трапезникова Москва, с. 107-114

 2000  Towards a unified toolset for embedded systems development 

Bahmurov A.G., Chistolinov M.V., Epatko I.V., Smelyanskij R.L., Vinter K., Zakharov V.A. в сборнике Proceedings of the conference UKRPROG-2000 “Problems of Programming “, том 1, с. 316-322

 2000  О международном проекте в области проверки правильности программного обеспечения встроенных систем 

Бахмуров А.Г., Захаров В.А., Смелянский Р.Л., Чистолинов М.В. в сборнике Программные системы и инструменты, место издания Изд-факультета ВМиК МГУ Москва, том 1, с. 24-31

 2000  О проблеме эквивалентности для схем программ с операторами засылки констант 

Захаров В.А. в сборнике Труды IV Международной конференции "Дискретные модели в теории управляющих систем", место издания МАКС-Пресс Москва, с. 153-154

 2000  О разрешимости проблемы эквивалентности в одном классе металинейных унарных рекурсивных программ 

Захаров В.А., Соколова К.А. в сборнике Труды IV Международной конференции "Дискретные модели в теории управляющих систем", место издания МАКС-Пресс Москва, с. 29-31

 2000  Общие методы построения разрешающих алгоритмов эквивалентности пропозициональных операторных программ 

Захаров В.А. в сборнике Труды IV Международной конференции "Дискретные модели в теории управляющих систем", место издания МАКС-Пресс Москва, с. 25-29

 2000  Операторные модели взаимодействующих процессов 

Захаров В.А., Незнанов И.К. в сборнике Математические вопросы кибернетики, место издания Физматлит Москва, том 9, с. 127-160

 2000  Формализация языка описания моделей распределенных систем программ при помощи временных автоматов 

Захаров В.А., Кончаков Р.В. в сборнике Труды Всероссийской научной конференции "Высокопроизводительные вычисления и их приложения", 30 октября - 2 ноября, Черноголовка, место издания МГУ, с. 151-157

 2000  Эффективные алгоритмы и их программные реализации 

Захаров В.А., Кузюрин Н.Н., Холодов А.Н. в сборнике Труды Института системного программирования, том 1, с. 115-124

 1999  On the refinement of logic programs by means of anti-unification 

Zakharov V.A. в сборнике Proceedings of the 2nd Panhellenic Logic Symposium, Delphi, место издания Greece, с. 219-224

 1999  О разрешимости проблемы эквивалентности в одном классе операторных программ 

Захаров В.А. в сборнике Прикладная математика и информатика, место издания МГУ Москва, том 5, с. 90-100

 1999  Об эффективной разрешимости проблемы эквивалентности линейных унарных рекурсивных программ 

Захаров В.А. в сборнике Математические вопpосы кибеpнетики, место издания Физматлит Москва, том 8, с. 255-273

 1998  An efficient and unified approach to the decidability of equivalence of propositional program schemes 

Zakharov V.A. в сборнике Proceedings of the 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13–17, 1998, серия Lecture Notes in Computer Science, место издания Springer-Verlag Berlin, том 1443, с. 247-259

 1998  Быстрые алгоритмы разрешения эквивалентности операторных программ на уравновешенных шкалах 

Захаров В.А. в сборнике Математические вопросы кибернетики, место издания Физматлит Москва, том 7, с. 303-324

 1998  О моделях систем взаимодействующих операторных программ 

Захаров В.А., Незнанов Н.К. в сборнике Труды III Международной конференции "Дискретные модели в теории управляющих систем", место издания Диалог - МГУ Москва, с. 75-79

 1998  О проблеме эквивалентности операторных программ на упорядоченных полугрупповых моделях 

Захаров В.А. в сборнике Труды III Международной конференции "Дискретные модели в теории управляющих систем", место издания Диалог - МГУ Москва, с. 36-40

 1997  On the verification of PLTL formulae by means of monotone disjunctive normal forms 

Zakharov V.A. в сборнике Proceedings of the 4th International Symposium "Logical Foundations of Computer Science", Yaroslavl, Russia, July 6–12, 1997, серия Lecture Notes in Computer Science, место издания Springer-Verlag Berlin, том 1234, с. 419-429

 1997  To the relationship between the interleaving and causal models of parallel computations 

Zakharov V.A., Spanopulo V.V. в сборнике Advances in Modal Logic'96, серия CSLI Lecture Notes, место издания CSLI Publications Ventura Hall, Stanford University, Stanford, CA 94305, с. 221-232

 1996  Быстрые алгоритмы распознавания эквивалентности в моделях программ с коммутирующими операторами 

Захаров В.А., Подловченко Р.И. в сборнике Компьютерные аспекты в научных исследованиях и учебном процессе, место издания Изд-Во Моск. Унив, с. 3-8

 1995  Эквивалентные преобразования схем программ в моделях, порожденных формулами динамической логики 

Захаров В.А. в сборнике Материалы XI международной конференции "Логика, методология, философия науки", место издания Институт философии РАН Москва, с. 137-142

 1994  О свободных схемах в формальных моделях программ 

Захаров В.А. в сборнике Математические вопросы кибернетики, место издания Физматлит Москва, том 5, с. 208-239

 1993  Об одном критерии сравнимости формальных моделей программ 

Захаров В.А. в сборнике Сборник трудов семинара по дискретной математики и ее приложениям, место издания Изд-во механико-математического факультета МГУ Москва, с. 2-4

 1993  Об одном типе эквивалентности схем программ 

Захаров В.А. в сборнике Методы и системы технической диагностики, место издания Саратовский государственный университет Саратов, том 18, с. 68-70

 1987  On the functional equivalence of Turing machines 

Zakharov V.A. в сборнике Proceedings of the 6-th International Conference "Fundamentals of Computation Theory", Kazan, USSR, June 22–26, 1987, серия Lecture Notes in Computer Science, издательство SPRINGER-VERLAG BERLIN (HEIDELBERGER PLATZ 3, BERLIN, GERMANY,D-14197), том 278, с. 488-492

Книги

2005  Embedding mobile ambients into pi-calculus

Ciobanu G., Zakharov V.A. место издания Universitatea “Alexandru Ioan Cuza Iasi, Romania, 17 с.

Тезисы докладов

2000  The development and verification of distributed real time embedded computer systems for avionics (Project DrTesy) 

Smeliansky R.L., Chistolinov M.V., Epatko I.V., Grote J.F., Konchakov R.V., Peshko A.S., Tsarkov D.V., Usenko Y.S., Winter K., Zakharov V.A. в сборнике Тезисы докладов четвертого сибирского конгресса по прикладной и индустриальной математике, том 2, тезисы, с. 128-129

 2012  О средстве трансляции моделей на языке UML во временные автоматы UPPAAL для верификации РВСРВ 

Захаров В.А., Зорин Д.А., Подымов В.В., Коннов И.В., Волканов Д.Ю. в сборнике Сборник трудов конференции "Моделирование - 2012". Киев, Украина, 2012, место издания Киев, тезисы, с. 199-202

 2010  Equivalence checking of sequential programs using two-tape automata 

Zakharov V.A. в сборнике International Workshop “Automata, algorithms and information technologies” (Kyev, May 19-21, 2010), место издания Abstracts Kiev, тезисы, с. 25-25

 2009  О сложности проверки эквивалентности программ с операторами засылки констант 

Захаров В.А., Щербина В.Л. в сборнике Tруды VIII Международной конференции «Дискре тные модели в теории управляющих систем», место издания М.: МАКС Пресс, тезисы, с. 369-374

 2008  О проблеме эквивалентности в одном классе монадических линейных программ 

Захаров В.А. в сборнике Тезисы докладов 15-ой международной конференции «Проблемы теоретической кибернетики» (Казань, 2-7 июня, 2008 г.), место издания Изд-во Казанского государственного университета Казань, тезисы, с. 40-40

 2008  Теоретические аспекты проблемы обфускации программ 

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В. в сборнике Тезисы доклада на XVII Общероссийской научно-технической конференции «Методы и технические средства обеспечения безопасности информации», С. Петербург, 7-11 июля 2008, тезисы

2007  Об эквивалентности программ с операторами, обладающими свойствами коммутативности и подавления 

Захаров В.А., Щербина В.Л. в сборнике Материалы IX Международного семинара «Дискретная математика и ее приложения» (Москва, 18-23 июня 2007 г.), место издания Изд-во механико-математического ф-та МГУ Москва, тезисы, с. 191-194

 2006  Применение методов теории игр к поиску некоторых видов симуляции на размеченных системах переходов 

Булычев П.Е., Захаров В.А., Коннов И.В. в сборнике Tруды VII Международной конференции «Дискре тные модели в теории управляющих систем», место издания М.: МАКС Пресс, тезисы, с. 40-46

 2005  Об одном символьном методе верификации криптографических протоколов 

Захаров В.А., Корчевский А.А. в сборнике Тезисы докладов XIV Международной конференции «Проблемы теоретической кибернетики» (Пенза, 23-28 мая 2005 г.), место издания Изд-во механико-математического ф-та МГУ Москва, тезисы, с. 71-71

 2005  Проверка эквивалентности программ: модели и алгоритмы 

Захаров В.А., Подловченко Р.И. в сборнике Тезисы докладов XIV Международной конференции «Проблемы теоретической кибернетики» (Пенза, 23-28 мая 2005 г.), место издания Изд-во механико-математического ф-та МГУ Москва, тезисы, с. 122-122

 2004  On the equivalence-checking problem for sequential programs with partially commuting and monotonic statements 

Zakharov V.A., Zakharyaschev I.M. в сборнике Proceedings of the XI Congress of Mathematics of Serbia and Montenegro, September 28-October 2, 2004, Petrovac, Montenegro, место издания Podgorica, Montenegro, тезисы, с. 79-79

 2002  Вычисление инвариантов последовательных программ 

Захаров В.А. в сборнике , Тезисы докладов XIII Международной конференции «Проблемы теоретической кибернетики", место издания Казанский государственный университет Казань, тезисы, с. 68-68

 2001  Верификация распределенных программ в системе имитационного моделирования DYANA 

Захаров В.А., Кончаков Р.В., Смелянский Р.Л., Царьков Д.В. в сборнике Тезисы докладов Международной научной конференции "Интеллектуальные и многопроцессорные системы", место издания Таганрог, тезисы, с. 152-156

 2000  On the approximation relation on dynamic logic models 

Zakharov V.A. в сборнике Abstracts of contributed papers. Logic Colloquium 2000, Paris, La Sorbonne, место издания Paris, тезисы, с. 23-31

 2000  On the logical and timed analysis of an airborne navigation system by means of DYANA 

Bahmurov A., Chistoliniv M., Konchakov R., Tsarkov D., Smelyanskij R., Zakharov V.A. в сборнике 4-th Multiconference of Systematic, Cybernetics and Informatics (SCI-2000), место издания Orlando, USA, тезисы

2000  The development and verification of distributed real time embedded computer systems for avionics 

Bahmurov A.G., Chistolinov M.V., Epatko I.V., Smelyanskij R.L., Vinter K., Zakharov V.A. в сборнике Тезисы докладов четвертого сибирского конгресса по прикладной и индустриальной математике, том 2, тезисы, с. 128-129

 1999  О проблеме эквивалентности унарных металинейных рекурсивных схем 

Захаров В.А. в сборнике Тезисы докладов XII международной конференции "Проблемы теоретической кибернетики", место издания Нижегородский государственный университет Нижний Новгород, тезисы, с. 78-78

 1998  О проблеме эквивалентности пропозициональных программ над полугруппами 

Захаров В.А. в сборнике Kurosh Algebraic Conference'98, Abstracts of Talks, место издания механико-математический факультет МГУ им. М.В. Ломоносова Москва, тезисы, с. 170-172

 1997  Полиномиальный алгоритм разрешения проблемы эквивалентности унарных линейных рекурсивных схем программ 

Захаров В.А. в сборнике Труды II Международной конференции «Дискре тные модели в теории управляющих Систем», место издания Диалог - МГУ Москва, тезисы, с. 26-29

 1996  Полиномиальный алгоритм разрешения эквивалентности схем программ 

Захаров В.А., Подловченко Р.И. в сборнике Тезисы докладов на XI Международной конференции по проблемам теоретической кибернетики, место издания Российский государственный гуманитарный университет Москва, тезисы, с. 68-70

 1996  Сравнительный анализ двух семантик параллельных вычислений 

Захаров В.А., Спанопуло В.В. в сборнике Тезисы докладов на XI Международной конференции по проблемам теоретической кибернетики, место издания г. Ульяновск, тезисы, с. 222-222

 1995  Вывод инвариантов программ с использованием антиунификации 

Захаров В.А. в сборнике Материалы 4-ой международной конференции по прикладной логике, место издания Иркутский государственный университет Иркутск, тезисы, с. 33-34

 1995  Моделирование логических программ пропозициональными схемами 

Захаров В.А., Болгов С.К. в сборнике Материалы 4-ой международной конференции по прикладной логике, место издания Иркутский государственный университет Иркутск, тезисы, с. 35-36

 1995  Проект смешанной операторно-логической системы программирования 

Захаров В.А., Маневич С.И. в сборнике Материалы 4-ой международной конференции по прикладной логике, место издания Иркутский государственный университет Иркутск, тезисы, с. 37-38

 1991  Условия свободной схемы в формальных моделях программ 

Захаров В.А. в сборнике Тезисы докладов IX Всесоюзной конференции "Проблемы теоретической кибернетики", место издания Волгоградский государственный университет Волгоград, тезисы, с. 94-96

 1988  Схемы Янова с автоматными сдвигами 

Захаров В.А. в сборнике Тезисы докладов VIII Всесоюзной конференции "Проблемы теоретической кибернетики", место издания Горьковский государственный университет Горький, тезисы, с. 101-102

 1985  Эквивалентные преобразования в одном классе машин Тьюринга 

Захаров В.А. в сборнике Прикладая математика и математическое обеспечение ЭВМ, место издания Московский государственный университет им. М.В. Ломоносова Москва, тезисы, с. 75-76

 1985  Эквивалентные преобразования моделей машин Тьюринга 

Захаров В.А. в сборнике Тезисы докладов VII Всесоюзной конф. "Проблемы теоретической кибернетики", место издания Иркутский государственный университет Иркутск, тезисы, с. 78-79

 1983  Проблема эквивалентности в одном классе машин Тьюринга 

Захаров В.А. в сборнике Тезисы докладов VI Всесоюзной конференции "Проблемы теоретической кибернетики", место издания Саратовский государственный университет Саратов, тезисы, с. 70-71