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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
Захаров Владимир Анатольевич
Захаров Владимир Анатольевич — доктор физико-математических наук, профессор.


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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


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

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


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


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 Network Update 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. в сборнике Proceedings 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. в сборнике Proceedings of the 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


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 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 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