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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
Строка 5: Строка 5:
 
== Области научных интересов ==
 
== Области научных интересов ==
  
−
===Модели программ===
+
=== Задача проверки эквивалентности программ ===
 +
Для формальных моделей последовательных, рекурсивных и параллельных программ исследуется проблема эквивалентности: верно ли, что две заданные произвольные программы имеют одинаковое поведение. Решение этой задачи находит применение при разработке оптимизирующих преобразований программ, при проведении реорганизации (рефакторинга) программ, при проектировании СБИС, при разработке антивирусных сканеров, при проверке стойкости криптографических протоколов.
  
−
Рассматриваются модели последовательных, рекурсивных и параллельных программ.        Исследуются проблемы эквивалентности и эквивалентных преобразований программ.
+
=== Обфускация программ ===
 +
Обфускация - это такая разновидность преобразований программ, которая сохраняет функциональные характеристики программ, но препятствует извлечению из открытого текста преобразованной программы полезной информации об устройстве ее алгоритма, структур данных, секретных ключей и пр. Основные задачи в этой области криптографии - разработка обфускирующих преобразований программ и оценка их стойкости, а также доказательство невозможности стойкой обфускации для тех или иных классов программ.
  
−
===Темпоральные логики===
+
=== Верификация моделей программ ===
−
 
+
Задача верификации моделей программ (model checking) состоит в том, чтобы для заданной модели программ, представленной системой переходов, выражением алгебры процессов, автоматом и пр., и спецификации программы, представленной формулой темпоральной логики, требуется проверки выполнимость спецификации на модели. В этом случае удается математически строго доказать, что проверяемая программа работает правильно.
−
Рассматриваются темпоральные логики линейного и ветвящегося времени.         Проектируются алгоритмы и программы, разрешающие проблему выполнимости в этих        логиках. Исследуются возможности применения темпоральных логик для спецификации         и верификации параллельных и распределенных программных систем.
+
−
 
+
−
===Логическое программирование===
+
  
 +
=== Логическое программирование ===
 
Разрабатываются и исследуются методы анализа логических программ.
 
Разрабатываются и исследуются методы анализа логических программ.
  
−
===Сети Петри===
+
=== Статический анализ программ ===
−
 
+
Статический анализ программ — это анализ программного обеспечения, производимый без реального выполнения исследуемых программ. Цель анализа - обнаружить зависимости по данным и по управлению между компонентами программы, которые можно использовать впоследствии для компиляции, оптимизации, верификации программ.
−
Решаются задачи анализа сетей Петри. Исследуются возможности применения сетей Петри        для моделирования параллельных и распределенных программных систем.
+
  
−
===Алгебры процессов===
+
=== Модели параллельных вычислений ===
 +
Конструируются и исследуются математические модели параллельных вычислений. Разрабатываются математические методы анализа моделей параллельных вычислений.
  
−
Рассматриваются задачи, связанные с применением различных алгебр процессов для        спецификации параллельных и распределенных программных систем.
+
=== Ссылки ===
 +
* [http://mathcyb.cs.msu.su/research.php#program_models Задача проверки эквивалентности программ]
 +
* [http://mathcyb.cs.msu.su/research.php#temp_logics Обфускация программ]
 +
* [http://mathcyb.cs.msu.su/research.php#temp_logics Верификация моделей программ]
 +
* [http://mathcyb.cs.msu.su/research.php#log_prog Логическое программирование]
 +
* [http://mathcyb.cs.msu.su/research.php#log_prog Статический анализ программ]
 +
* [http://mathcyb.cs.msu.su/research.php#petri_nets Модели параллельных вычислений]
  
 
== Лекционные курсы ==
 
== Лекционные курсы ==

Версия 13:53, 26 декабря 2013

Захаров Владимир Анатольевич
Захаров Владимир Анатольевич — профессор. Заведующий лабораторией математических проблем компьютерной безопасности.


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

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

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

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

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

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

Задача верификации моделей программ (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=396»