Захаров Владимир Анатольевич
- Ведущий научный сотрудник:Факультет компьютерных наук / Научно-учебная лаборатория процессно-ориентированных информационных систем (ПОИС)
- Начал работать в НИУ ВШЭ в 2015 году.
Образование, учёные степени
- 2012Доктор физико-математических наук
- 1982
Специалитет: Московский государственный университет им. М.В. Ломоносова, специальность «Прикладная математика»
Научный руководитель диссертационных исследований
2015 Быстрые алгоритмы проверки эквивалентности программ в моделях с полугрупповой семантикой
Кандидатская диссертация по специальности 01.01.09 - Дискретная математика и математическая кибернетика (физ.-мат. науки)
Подымов Владислав Васильевич, МГУ имени М.В. Ломоносова
- Защищена в совете Д 501.001.44 при МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- 2010 Алгоритмы вычисления отношений подобия в задачах верификации и реструктуризации программ Кандидатская диссертация по специальности 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей (физ.-мат. науки)Булычев П.Е.
- Защищена в совете Д 501.001.44 при МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- 2008 Алгоритмы антиунификации и их применение для вычисления инвариантов программ
- Кандидатская диссертация по специальности 01.01.09 - Дискретная математика и математическая кибернетика (физ.-мат. науки)
- Костылев Е.В.
- Защищена в совете Д 501.001.44 при МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- 2008 Верификация параметризованных моделей распределенных систем
- Кандидатская диссертация по специальности 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей (физ.-мат. науки)
- Коннов И.В.
- Защищена в совете Д 501.001.44 при МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- 2002 Верификация распределенных программ методом проверки на модели
- Кандидатская диссертация по специальности 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей (физ.-мат. науки)
- Царьков Дмитрий Викторович
- Защищена в совете Д 501.001.44 при МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- 2002 Вопросы сложности анализа конъюнктивных грамматик
- Кандидатская диссертация по специальности 01.01.09 - Дискретная математика и математическая кибернетика (физ.-мат. науки)
- Охотин А.С.
- Защищена в совете Д 501.001.44 при МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
20202
- Статья Gnatenko A., Zakharov V. Using an extension of CTL* for specification and verification of sequential reactive systems // Системная информатика. 2020. Vol. 17. P. 21-32.
- Статья Захаров В. А. Эффективные алгоритмы проверки эквивалентности для некоторых классов автоматов // Моделирование и анализ информационных систем. 2020. Т. 27. № 3. С. 260-303. doi
20196
- Статья Zakharov V., Abbas M. M. Even Simple Processes of Pi-calculus are Hard for Analysis / Пер. с рус. // Automatic Control and Computer Sciences, USA. 2019. Vol. 53. No. 7. P. 589-606. doi
- Статья Gnatenko A., Zakharov V. On the Expressive Power of Some Extensions of Linear Temporal Logic / Пер. с рус. // Automatic Control and Computer Sciences. 2019. Vol. 53. No. 7. P. 663-675. doi
- Глава книги Гнатенко А. Р., Захаров В. А. Верификация моделей реагирующих систем относительно одного расширения темпоральной логики CTL* // В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2019. С. 263-266.
- Статья Захаров В. А., Абрамова И. В., Варновский Н. П., Шокуров А. В. О возможности стойкой обфускации программ в одной модели облачных вычислений // Труды Института системного программирования РАН. 2019. Т. 31. № 6. С. 145-162. doi
- Глава книги Захаров В. А., Винарский Е. М. О задаче верификации для одного класса автоматов реального времени // В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2019. С. 257-260.
- Глава книги Захаров В. А., Жайлауова Ш. Р. О проблеме эквивалентности недетерминированных автоматов-преобразователей над однобуквенным выходным алфавитом // В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2019. С. 272-274.
20187
- Статья Gnatenko A., Zakharov V. On the Model Checking of Finite State Transducers over Semigroups // Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 303-324. doi
- Глава книги Zakharov V., Gnatenko A. On the expressive power of some extensions of Linear Temporal Logic, in: Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018 / Ed. by V. Zakharov, Н. В. Шилов. Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018. P. 29-36.
- Книга Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018 / Ed. by V. Zakharov, Н. В. Шилов. Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018.
- Статья Захаров В. А., Аббас М. М. Даже простые процессы pi-исчисления трудны для анализа // Моделирование и анализ информационных систем. 2018. Т. 25. № 6. С. 589-606. doi
- Статья Гнатенко А. Р., Захаров В. А. О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. 2018. Т. 25. № 5. С. 506-524. doi
- Глава книги Захаров В. А. Полиномиальный алгоритм проверки эквивалентности детерминированных двухленточных автоматов // В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды / Под общ. ред.: Д. С. Романов. МГУ, МАКС Пресс, 2018. С. 128-130.
- Глава книги Гнатенко А. Р., Захаров В. А. Языки спецификаций моделей Крипке на основе темпоральных логик и их выразительные возможности // В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды / Под общ. ред.: Д. С. Романов. МГУ, МАКС Пресс, 2018. С. 131-133.
20177
- Статья Zakharov V., Jaylauova S. On the Minimization Problem for Sequential Programs / Пер. с рус.: V. Zakharov. // Automatic Control and Computer Sciences. 2017. Vol. 51. No. 7. P. 689-700.
- Статья Zakharov V., Temerbekova G. On the Minimization of Finite State Transducers over Semigroups / Пер. с рус.: V. Zakharov. // Automatic Control and Computer Sciences. 2017. Vol. 51. No. 7. P. 523-530.
- Статья Zakharov V., Varnovsky N., Shokurov A. On the deductive security of queries to confidential databases in cloud computing systems / Пер. с рус.: V. Zakharov. // Moscow University Computational Mathematics and Cybernetics. 2017. Vol. 41. No. 1. P. 60-70. doi
- Статья Захаров В. А., Варновский Н. П., Шокуров А. В. О дедуктивной безопасности запросов к базам конфиденциальных данных в системе облачных вычислений // Вестник Московского университета. Серия 15: Вычислительная математика и кибернетика. 2017. № 1. С. 38-44.
- Статья Захаров В. А., Жайлауова Ш. Р. О задаче минимизации последовательных программ // Моделирование и анализ информационных систем. 2017. Т. 24. № 4. С. 415-433. doi
- Глава книги Захаров В. А., Жайлауова Ш. Р. О минимизации схем программ относительно логико-термальной эквивалентности // В кн.: Проблемы теоретической кибернетики: XVIII международная конференция (Пенза, 19-23 июня 2017 г.). М. : МГУ, МАКС Пресс, 2017. С. 84-87.
- Глава книги Захаров В. А., Гнатенко А. Р. О сложности верификации автоматов-преобразователей над коммутативными полугруппами // В кн.: Проблемы теоретической кибернетики: XVIII международная конференция (Пенза, 19-23 июня 2017 г.). М. : МГУ, МАКС Пресс, 2017. С. 68-71.
201611
- Статья Zakharov V., Varnovsky N., Shokurov A. On the existence of provably secure cloud computing systems / Пер. с рус.: V. Zakharov. // Moscow University Computational Mathematics and Cybernetics. 2016. Vol. 36. No. 2. P. 83-88.
- Статья Zakharov V., Temerbekova G. On the minimization and equivalence checking of sequential reactive systems // Системная информатика. 2016. No. 7. P. 33-44.
- Глава книги Zakharov V., Kozlova D. On the model checking of sequential reactive systems, in: Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, 2016. Vol. 1698. Humboldt-Universität zu Berlin, 2016. P. 233-244.
- Глава книги Захаров В. А., Варновский Н. П., Шокуров А. В. К вопросу о дедуктивной безопасности вычислений над зашифрованными данными // В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2016. С. 371-373.
- Статья Захаров В. А., Варновский Н. П., Шокуров А. В. К вопросу о существовании доказуемо стойких систем облачных вычислений // Вестник Московского университета. Серия 15: Вычислительная математика и кибернетика. 2016. № 2. С. 32-38.
- Статья Захаров В. А., Темербекова Г. Г. О минимизации конечных автоматов-преобразователей над полугруппами // Моделирование и анализ информационных систем. 2016. Т. 23. № 6. С. 741-753.
- Глава книги Захаров В. А., Попеско У. В. О проблеме логико-термальной эквивалентности недетерминированных стандартных схем программ // В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2016. С. 196-198.
- Глава книги Захаров В. А., Джусупекова З. А. О проверке k-значности конечных автоматов-преобразователей над полугруппами // В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2016. С. 190-192.
- Глава книги Захаров В. А., Темербекова Г. Г. Оптимизирующие преобразования потоковых программ // В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2016. С. 232-234.
- Книга Захаров В. А. Проблема эквивалентности программ: модели, алгоритмы, сложность. АРГАМАК-МЕДИА, 2016.
- Глава книги Захаров В. А., Козлова Д. Г. Темпоральная логика для верификации автоматов-преобразователей // В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2016. С. 204-206.
201511
- Статья Zakharov V.A., Volkanov D. Y., Zorin D., Konnov I., Podymov V.V. A Combined Toolset for the Verification of Real-Time Distributed Systems / Пер. с рус. // Programming and Computer Software. 2015. Vol. 41. No. 6. P. 325-335.
- Статья Zakharov V.A. Equivalence Checking Problem for Finite State Transducers // Lecture Notes in Computer Science. 2015. Vol. 9270. P. 208-221.
- Статья Zakharov V., Чемерицкий Е. В. On Network Update Problems for Software Defined Networks / Пер. с рус.: V. Zakharov. // Automatic Control and Computer Sciences. 2015. Vol. 49. No. 7 (в печати)
- Статья Zakharov V.A., Kuzurin N., Varnovsky N., Shokurov A. The Current State of Art in Program Obfuscations: Definitions of Obfuscation Security / Пер. с рус. // Programming and Computer Software. 2015. Vol. 41. No. 6. P. 361-372.
- Статья Алтухов В., Захаров В. А., Подымов В. В., Чемерицкий Е. VERMONT - средство верификации программно-конфигурируемых сетей // Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Информатика. Телекоммуникации. Управление. 2015. Т. 212. № 1. С. 74-87.
- Глава книги Захаров В. А., Шокуров А. В., Варновский Н. П. К вопросу о существовании доказуемо стойких систем облачных вычислений // В кн.: Дискретные модели в теории управляющих систем : IX Международная конференция, Москва и Подмосковье, 20-22 мая 2015 г.: Труды. М. : МАКС Пресс, 2015. С. 50-52.
- Статья Захаров В. А., Волканов Д. Ю., Зорин Д. А., Коннов И. В., Подымов В. В. Комбинированное средство верификации распределённых вычислительных систем реального времени // Программирование. 2015. № 6. С. 72-86.
- Глава книги Захаров В. А., Новикова Т. А. Логико-термальная эквивалентность программ с динамической памятью // В кн.: Дискретные модели в теории управляющих систем : IX Международная конференция, Москва и Подмосковье, 20-22 мая 2015 г.: Труды. М. : МАКС Пресс, 2015. С. 173-176.
- Статья Захаров В. А. Моделирование и анализ поведения последовательных реагирующих программ // Труды Института системного программирования РАН. 2015. Т. 27. № 2. С. 221-250.
- Статья Захаров В. А., Подымов В. В. Применение алгоритмов проверки эквивалентности для оптимизации программ // Труды Института системного программирования РАН. 2015. Т. 27. № 4
- Статья Захаров В. А., Кузюрин Н. Н., Варновский Н. П., Шокуров А. В. Современное состояние исследований в области обфускации программ: определение стойкости обфускации // Программирование. 2015. № 6 (в печати)
201411
- Статья Smeliansky R., Chemeritsky E., Zakharov V. A formal model and verification problems for Software Defined Networks / Пер. с рус.: V. Zakharov. // Automatic Control and Computer Sciences. 2014. Vol. 48. No. 7. P. 398-406.
- Глава книги Zakharov V., Чемерицкий Е. В. Consistent network update without tagging, in: Proceedings of 2014 International Science and Technology Conference "Modern Networking Technologies (MoNeTec): SDN&NFV Next Generation of Computational Infrastructure", Moscow, Russia, October 27-29, 2014. M. : Max press, 2014. P. 47-52.
- Статья Konnov I., Podymov V.V., Volkanov D., Zorin D., Zakharov V.A. How to make a simple tool for verification of real-time systems / Пер. с рус. // Automatic Control and Computer Sciences. 2014. Vol. 48. No. 7. P. 534-542.
- Глава книги Zakharov V., Новикова Т. А. Two-sided unification is NP-complete, in: Proceedings of the 28th International Workshop on Unification, UNIF 2014. Technical report no. 14-06 in RISC Report Series. Linz : Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, 2014. P. 55-61.
- Глава книги Zakharov V., Подымов В. В., Алтухов В. С., Чемерицкий Е. В. VERMONT - a toolset for checking SDN packet forwarding policies on-line, in: Proceedings of 2014 International Science and Technology Conference "Modern Networking Technologies (MoNeTec): SDN&NFV Next Generation of Computational Infrastructure", Moscow, Russia, October 27-29, 2014. M. : Max press, 2014. P. 7-12.
- Статья Захаров В. А., Новикова Т. А. Двусторонняя унификация программ и ее применение для задач рефакторинга // Труды Института системного программирования РАН. 2014. Т. 26. № 2. С. 245-268.
- Статья Захаров В. А., Чемерицкий Е. В. О некоторых задачах реконфигурирования программно-конфигурируемых сетей // Моделирование и анализ информационных систем. 2014. Т. 21. № 6. С. 57-69.
- Глава книги Захаров В. А., Новикова Т. А. О сложности задачи решения линейных уравнений над конечными подстановками // В кн.: Материалы XVII международной конференции "Проблемы теоретической кибернетики". Каз. : Отечество, 2014. С. 221-223.
- Глава книги Захаров В. А. Об эквивалентности ограниченно недетерминированных автоматов-преобразователей над полугруппами // В кн.: Материалы XVII международной конференции "Проблемы теоретической кибернетики". Каз. : Отечество, 2014. С. 100-102.
- Статья Подымов В. В., Захаров В. А. Полиномиальный алгоритм проверки эквивалентности в модели программ с перестановочными и подавляемыми операторами // Труды Института системного программирования РАН. 2014. Т. 26. № 3. С. 145-166.
- Статья Захаров В. А., Варновский Н. П., Кузюрин Н. Н., Шокуров А. В. Современное состояние исследований в области обфускации программ: определения стойкости обфускации // Труды Института системного программирования РАН. 2014. Т. 26. № 3. С. 167-198.
20131
20123
- Статья Волканов Д., Захаров В. А., Зорин Д., Коннов И., Подымов В. В. Как разработать простое средство верификации систем реального времени // Моделирование и анализ информационных систем. 2012. Т. 19. № 6. С. 45-56.
- Статья Захаров В. А., Новикова Т. А. Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ // Труды Института системного программирования РАН. 2012. Т. 22. С. 435-455.
- Статья Захаров В. А., Новикова Т. А. Унификация программ // Труды Института системного программирования РАН. 2012. Т. 23. С. 455-476.
20111
20104
- Статья Zakharov V., Коннов И. В. An invariant-based approach to the verification of asynchronous parameterized networks // Journal of symbolic computation. 2010. Vol. 45. No. 11. P. 1144-1162.
- Статья Захаров В. А., Коннов И. В. Адаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времени // Моделирование и анализ информационных систем. 2010. Т. 17. № 4. С. 78-87.
- Статья Захаров В. А., Подымов В. В. Об одной полугрупповой модели программ, определяемой при помощи двухленточных автоматов // Научные ведомости Белгородского государственного университета. Серия: История. Политология. Экономика. Информатика. 2010. Т. 14. № 7. С. 94-101.
- Статья Захаров В. А. Проверка эквивалентности программ при помощи двухленточных автоматов // Cybernetics and Systems Analysis. 2010. № 4. С. 39-48.
Участие в редколлегиях научных журналов
С 2016 г.: член редколлегии журнала «Моделирование и анализ информационных систем».
Гранты
Грант РФФИ 15-01-05742 "Теория схем программ в задачах оптимизации, верификации и реорганизации последовательных и параллельных программ"
Опыт работы
Московский государственный университет им. М.В. Ломоносова, факультет ВМК, 1986 - наст. время.
Институт прикладной математики им. М.В. Келдыша, 1991-2004.
Институт системного программирования, 2000 - наст. время
Национальный Исследовательский Университет "Высшая школа экономики", 2015 - наст. время.
Выездной семинар «Процессно-ориентированные информационные системы»
27-29 ноября в учебном центре «Вороново» состоялся выездной семинар «Процессно-ориентированные информационные системы» научно-учебной лаборатории ПОИС под руководством профессора И.А.Ломазовой. В мероприятии приняли участие сотрудники лаборатории и исследователи из Москвы и Ярославля. Участники семинара обсудили актуальные научные исследования в области process mining и в смежных областях.