Участник:ZakharovVA — различия между версиями

Версия 15:34, 29 сентября 2014

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 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 Математические проблемы обфускации

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

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

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

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

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

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

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

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 О проблеме эквивалентности для программ с частично перестановочными и монотонными операторами

Захаров В.А., Захарьящев И.М. в сборнике Труды 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