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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1. Формальные модели программ и свободные схемы // Программирование, 1992, N 2, с.10-24
  2. Об одном критерии сравнимости операторных формальных моделей программ // Программирование, 1993, N 4, с.12-25
  3. О свободных схемах в формальных моделях программ // Математические вопросы кибернетики, 1994, вып. 5, с.208-239
  4. Условия сглаживаемости операторных формальных моделей программ // Программирование, 1994, N 5, с.23-40
  5. О преобразованиях операторных процедур в логические программы // Программирование, 1994, N 6, с.23-39 (совм. с Маневичем С. И.)
  6. Об отношении аппроксимируемости семантик операторных программ // Вестник Московского университета, сер. 15, Вычислительная математика и кибернетика, 1994, N 4, с.54-60
  7. О взаимосвязи двух семантик параллельных вычислений (PostScript) // Программирование, 1997, N 6, с.36-48 (совм. с Спанопуло В. В.)
  8. To the Relationship between the Interleaving and Causal Models of Parallel Computations (PostScript) // Advances in Modal Logic'96, CSLI Publications,1997, p.221-232 (совм. с Спанопуло В. В.)
  9. On the verification of PLTL formulae by means of monotone disjunctive normal forms (PostScript) // Lecture Notes in Computer Science, Springer-Verlag, 1997, v.1234, p.419-429
  10. Полиномиальный алгоритм разрешения проблемы эквивалентности унарных линейных рекурсивных схем программ (PostScript) // Сборник трудов II Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-97, с.26-29
  11. О проблеме эквивалентности операторных схем на упорядоченных полугрупповых моделях (PostScript) // Сборник трудов III Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-98, с.36-40
  12. О моделях систем взаимодействующих операторных программ моделях (PostScript) // Сборник трудов III Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-98, с.36-40 (совм. с Незнановым И. К.)
  13. О восстановлении процесса по последовательности срабатывания переходов сети Петри (PostScript) // Вестник Московского университета, сер. 15, Вычислительная математика и кибернетика, 1998, N 4, с.31-34
  14. Полиномиальный по сложности алгоритм, распознающий коммутативную эквивалентность схем программ (PostScript) // Доклады РАН, 1998, т. 362, N 6 (совм. с Подловченко Р. И.)
  15. Эффективные алгоритмы проверки выполнимости формул темпоральной логики CTL и их применение для верификации параллельных программ (PostScript) // Программирование, 1998, N 4 (совм. с Царьковым Д. В.)
  16. An Efficient and Unified Approac to the Decidability of Equivalence of Propositional Program Schemes (PostScript) // Lecture Notes in Computer Science, Springer-Verlag, 1998, v.1443, p.247-259.
  17. Быстрые алгоритмы разрешения эквивалентности операторных программ на упорядоченных шкалах (PostScript) // Математические вопросы кибернетики, 1998, вып. 7, с.303-324
  18. Аппроксимация абстрактных семантик формальными моделями программ // Дискретная математика, 1998, том 10, вып. 4, с.119-141
  19. Об эффективной разрешимости проблемы эквивалентности линейных унарных рекурсивных программ (PostScript) // Математические вопросы кибернетики, 1999, вып. 8, с.255-273
  20. On the refinement of logic programs by means of anti-unification (PostScript) // Proceedings of the 2nd Panhellenic Logic Symposium, Delphi, Greece, 1999, p.219-224.
  21. Быстрые алгоритмы разрешения эквивалентности пропозициональных операторных программ на упорядоченных полугрупповых шкалах (PostScript) // Вестник Московского университета, сер. 15, Вычислительная математика и кибернетика, 1999, N 3, с.29-35
  22. О разрешимости проблемы эквивалентности в одном классе операторных программ (PostScript) // Сборник "Прикладная математика и информатика", Изд-во ВМиК МГУ, 1999, вып. 5 с.99-100
  23. On the decidability of the equivalence problem for orthogonal sequential programs (PostScript) // Grammars, Kluer Academic Publishers, 1999, v.2, N 3, p.271-281
  24. Общие методы построения разрешающих алгоритмов для проблемы эквивалентности пропозициональных операторных программ (PostScript) // Сборник трудов IV Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-00, с.25-29
  25. О разрешимости проблемы эквивалентности в одном классе металинейных унарных рекурсивных программ (PostScript) // Сборник трудов IV Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-00, с.29-31 (совм. с Соколовой К. А.)
  26. О проблеме эквивалентности для схем программ с операторами засылки констант (PostScript) // Сборник трудов IV Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-00, с.153-154
  27. On the Decidability of the Equivalence Problem for Monadic Recursive Programs (PostScript) // Theoretical Information and Applications, 2000, v.34, N 2, p.157-171
Источник — «https://mk.cs.msu.ru/index.php?title=Участник:ZakharovVA&oldid=444»