Участник:ZakharovVA
Содержание
Области научных интересов
Модели программ
Рассматриваются модели последовательных, рекурсивных и параллельных программ. Исследуются проблемы эквивалентности и эквивалентных преобразований программ.
Темпоральные логики
Рассматриваются темпоральные логики линейного и ветвящегося времени. Проектируются алгоритмы и программы, разрешающие проблему выполнимости в этих логиках. Исследуются возможности применения темпоральных логик для спецификации и верификации параллельных и распределенных программных систем.
Логическое программирование
Разрабатываются и исследуются методы анализа логических программ.
Сети Петри
Решаются задачи анализа сетей Петри. Исследуются возможности применения сетей Петри для моделирования параллельных и распределенных программных систем.
Алгебры процессов
Рассматриваются задачи, связанные с применением различных алгебр процессов для спецификации параллельных и распределенных программных систем.
Лекционные курсы
- Математическая логика и логическое программирование
- Математическая логика и теория множеств
- Введение в теорию алгоритмов
- Введение в теорию автоматов
- Темпоральные логики и их применение для анализа программ
Избранные публикации
- Формальные модели программ и свободные схемы // Программирование, 1992, N 2, с.10-24
- Об одном критерии сравнимости операторных формальных моделей программ // Программирование, 1993, N 4, с.12-25
- О свободных схемах в формальных моделях программ // Математические вопросы кибернетики, 1994, вып. 5, с.208-239
- Условия сглаживаемости операторных формальных моделей программ // Программирование, 1994, N 5, с.23-40
- О преобразованиях операторных процедур в логические программы // Программирование, 1994, N 6, с.23-39 (совм. с Маневичем С. И.)
- Об отношении аппроксимируемости семантик операторных программ // Вестник Московского университета, сер. 15, Вычислительная математика и кибернетика, 1994, N 4, с.54-60
- О взаимосвязи двух семантик параллельных вычислений (PostScript) // Программирование, 1997, N 6, с.36-48 (совм. с Спанопуло В. В.)
- To the Relationship between the Interleaving and Causal Models of Parallel Computations (PostScript) // Advances in Modal Logic'96, CSLI Publications,1997, p.221-232 (совм. с Спанопуло В. В.)
- 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
- Полиномиальный алгоритм разрешения проблемы эквивалентности унарных линейных рекурсивных схем программ (PostScript) // Сборник трудов II Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-97, с.26-29
- О проблеме эквивалентности операторных схем на упорядоченных полугрупповых моделях (PostScript) // Сборник трудов III Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-98, с.36-40
- О моделях систем взаимодействующих операторных программ моделях (PostScript) // Сборник трудов III Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-98, с.36-40 (совм. с Незнановым И. К.)
- О восстановлении процесса по последовательности срабатывания переходов сети Петри (PostScript) // Вестник Московского университета, сер. 15, Вычислительная математика и кибернетика, 1998, N 4, с.31-34
- Полиномиальный по сложности алгоритм, распознающий коммутативную эквивалентность схем программ (PostScript) // Доклады РАН, 1998, т. 362, N 6 (совм. с Подловченко Р. И.)
- Эффективные алгоритмы проверки выполнимости формул темпоральной логики CTL и их применение для верификации параллельных программ (PostScript) // Программирование, 1998, N 4 (совм. с Царьковым Д. В.)
- 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.
- Быстрые алгоритмы разрешения эквивалентности операторных программ на упорядоченных шкалах (PostScript) // Математические вопросы кибернетики, 1998, вып. 7, с.303-324
- Аппроксимация абстрактных семантик формальными моделями программ // Дискретная математика, 1998, том 10, вып. 4, с.119-141
- Об эффективной разрешимости проблемы эквивалентности линейных унарных рекурсивных программ (PostScript) // Математические вопросы кибернетики, 1999, вып. 8, с.255-273
- 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.
- Быстрые алгоритмы разрешения эквивалентности пропозициональных операторных программ на упорядоченных полугрупповых шкалах (PostScript) // Вестник Московского университета, сер. 15, Вычислительная математика и кибернетика, 1999, N 3, с.29-35
- О разрешимости проблемы эквивалентности в одном классе операторных программ (PostScript) // Сборник "Прикладная математика и информатика", Изд-во ВМиК МГУ, 1999, вып. 5 с.99-100
- On the decidability of the equivalence problem for orthogonal sequential programs (PostScript) // Grammars, Kluer Academic Publishers, 1999, v.2, N 3, p.271-281
- Общие методы построения разрешающих алгоритмов для проблемы эквивалентности пропозициональных операторных программ (PostScript) // Сборник трудов IV Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-00, с.25-29
- О разрешимости проблемы эквивалентности в одном классе металинейных унарных рекурсивных программ (PostScript) // Сборник трудов IV Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-00, с.29-31 (совм. с Соколовой К. А.)
- О проблеме эквивалентности для схем программ с операторами засылки констант (PostScript) // Сборник трудов IV Международной конференции "Дискретные модели в теории управляющих систем", Красновидово-00, с.153-154
- On the Decidability of the Equivalence Problem for Monadic Recursive Programs (PostScript) // Theoretical Information and Applications, 2000, v.34, N 2, p.157-171