Захаров Владимир Анатольевич
email: zakh@cs.msu.su
Содержание
Области научных интересов
Задача проверки эквивалентности программ
Для формальных моделей последовательных, рекурсивных и параллельных программ исследуется проблема эквивалентности: верно ли, что две заданные произвольные программы имеют одинаковое поведение. Решение этой задачи находит применение при разработке оптимизирующих преобразований программ, при проведении реорганизации (рефакторинга) программ, при проектировании СБИС, при разработке антивирусных сканеров, при проверке стойкости криптографических протоколов.
Обфускация программ
Обфускация - это такая разновидность преобразований программ, которая сохраняет функциональные характеристики программ, но препятствует извлечению из открытого текста преобразованной программы полезной информации об устройстве ее алгоритма, структур данных, секретных ключей и пр. Основные задачи в этой области криптографии - разработка обфускирующих преобразований программ и оценка их стойкости, а также доказательство невозможности стойкой обфускации для тех или иных классов программ.
Верификация моделей программ
Задача верификации моделей программ (model checking) состоит в том, чтобы для заданной модели программ, представленной системой переходов, выражением алгебры процессов, автоматом и пр., и спецификации программы, представленной формулой темпоральной логики, требуется проверки выполнимость спецификации на модели. В этом случае удается математически строго доказать, что проверяемая программа работает правильно.
Логическое программирование
Разрабатываются и исследуются методы анализа логических программ.
Статический анализ программ
Статический анализ программ — это анализ программного обеспечения, производимый без реального выполнения исследуемых программ. Цель анализа - обнаружить зависимости по данным и по управлению между компонентами программы, которые можно использовать впоследствии для компиляции, оптимизации, верификации программ.
Модели параллельных вычислений
Конструируются и исследуются математические модели параллельных вычислений. Разрабатываются математические методы анализа моделей параллельных вычислений.
Программно конфигурируемые сети
Программно-коммутируемые сети (ПКС) --- это класс компьютерных телекоммуникационных сетей, появившийся несколько лет назад в стремлении упростить проектирование и повысить гибкость управления сетями за счет разделения потоков данных (пакетов) и потоков управления (сообщений и команд), циркулирующие в сетях. ПКС представляет собой распределенную систему, в которой один или несколько контроллеров управляют множеством сетевых коммутаторов, обеспечивающих продвижение пакетов по каналам сети. Функциональные возможности и порядок взаимодействия коммутаторов и контроллеров ПКС определяются протоколом OpenFlow. Конструируются и исследуются формальные модели ПКС, разрабатываются методы и алгоритмы решения задач верификации и реконфигурации ПКС.
Лекционные курсы
- Математическая логика и теория алгоритмов ((3 семестр))
- Математическая логика и логическое программирование (3-й поток) (7 семестр)
- Модели вычислений (8 семестр)
- Распределенные алгоритмы (10 семестр)
- Математические методы верификации схем и программ (11 семестр)
- Модели последовательных и параллельных вычислений (12 семестр)
Спецсеминары
Аспиранты и студенты
- Подымов Владислав Васильевич
- Новикова Татьяна Анатольевна
- Попеско Ульна Владиславовна
Избранные публикации
Статьи в журналах
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
Захаров В.А., Коннов И.В. в журнале Моделирование и анализ информационных систем, том 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
Булычев П.Е., Захаров В.А. в журнале Вестник МЭИ, № 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
Захаров В.А. в журнале Вестник Московского университета. Серия 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
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
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
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
Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В., Чернов А.В. в сборнике Труды Института Системного программирования, место издания ИСП РАН, том 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
Захаров В.А., Захарьящев И.М., Подловченко Р.И., Русаков Д.М., Щербина В.Л. в сборнике Труды второй всероссийской конференции «Методы и средства обработки информации», место издания Изд-во ф-та ВМК МГУ Москва, с. 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
Захаров В.А. в сборнике Труды 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 2-nd Panhellenic Logic Symposium, Delphi, место издания Greece, p. 219-224
1999 О разрешимости проблемы эквивалентности в одном классе операторных программ
Захаров В.А. в сборнике Прикладная математика и информатика, место издания МГУ Москва, том 5, с. 90-100
1999 Об эффективной разрешимости проблемы эквивалентности линейных унарных рекурсивных программ
Захаров В.А. в сборнике Математические вопpосы кибеpнетики, место издания Физматлит Москва, том 8, с. 255-273
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
