Кафедра математической кибернетики - Вклад участника [ru]

Обобщенная выполнимость

2025-08-25T16:53:11Z

Root: Root переименовал страницу Дискретные функции и выполнимость ограничений в Обобщенная выполнимость

[[Категория:Лекционные курсы кафедры МК]]
[[Категория:Магистерская программа Дискретные структуры и алгоритмы]]
[[Категория:Спецкурсы кафедры МК]]
Обязательный курс для студентов 518/1 группы магистерской программы "Дискретные структуры и алгоритмы".

Спецкурс для студентов магистратуры.

Лектор - [[Селезнева Светлана Николаевна]]

Лекции - 2 ч в неделю.

Семинары - 1 ч в неделю (для студентов 518/1 группы).

'''Аннотация'''. Курс посвящен рассмотрению подходов к изучению теоретической вычислительной сложности задач обобщенной выполнимости. Задача обобщенной выполнимости состоит в выяснении выполнимости системы отношений, принадлежащих заранее известному множеству S и связывающих произвольные переменные. При этом полагается, что в множество S входят отношения на конечном множестве, содержащем k элементов. Известная задача выполнимости КНФ является частным случаем этой задачи. В курсе подробно разбирается случай k=2, описываются все виды множеств S, при которых задача обобщенной выполнимости может быть решена полиномиальными алгоритмами, и показывается ее труднорешаемость во всех других случаях. Разбирается общий подход к изучению вычислительной сложности этой задачи при произвольных k.

==Объявления==



==Лекции==

'''Часть 1. Повторение'''.

Лекция 1. Вступление. Алгебра логики. Функции алгебры логики. Формулы. Полнота. Замкнутые классы. Классы T_0, T_1, L, S, M. Теорема Поста.

Лекция 2. Конъюнктивные нормальные формы. Имплицента, простая имплицента функции. Сокращенная КНФ функции. Способы построения сокращенной КНФ.

Лекция 3. Полином Жегалкина. Способы построения полинома Жегалкина функции. Линейная имплицента функции. Линейная конъюнктивная нормальная форма (ЛКНФ). Линейная соимплицента функции. Поиск всех линейных соимплицент функции.

Лекция 4. Задачи распознавания. Вычислительная сложность задачи. Классы P и NP, NP-полные задачи. NP-полнота задачи 3-раскраски графов. Задачи обобщенной выполнимости.

Коллоквиум 1.

'''Часть 2. Обобщенная выполнимость'''.

Лекция 5. Слабо положительные и слабо отрицательные КНФ и функции. Критерии слабой положительности и слабой отрицательности функции. Полиномиальные алгоритмы проверки выполнимости слабо положительной и слабо отрицательной КНФ.

Лекция 6. Биюнктивные КНФ и функции. Критерий биюнктивности функции. Полиномиальные алгоритмы проверки выполнимости биюнктивной КНФ. Полиномиальный алгоритм поиска решения выполнимой биюнктивной КНФ.

Лекция 7. ЛКНФ и мультиаффинные функции. Критерий мультиаффинности функции. Полиномиальный алгоритм проверки выполнимости ЛКНФ. Полиномиальный алгоритм проверки по полиному Жегалкина представимости функции в виде ЛКНФ. Функции, сохраняющие константу.

Лекция 8. Условная выразимость функций. Леммы об условной выразимости. Лемма о функции, не сохраняющий единицу, и о функции, сохраняющей ноль. Лемма о несамодополнительной функции. Лемма о самодополнительной функции.

Лекция 9. Лемма о не слабо положительной функции и не слабо отрицательной функции. Лемма о небиюнктивной функции и немультиаффинной функции. Условная выразимость дизъюнкции трех литералов.

Лекция 10. Теорема Шефера о разделимости вычислительной сложности задач обобщенной выполнимости. Задачи обобщенной выполнимости с бесконечным множеством.

Коллоквиум 2.

'''Часть 3. Общий подход'''.

Лекция 11. Отношения на конечном множестве. Формулы, S-формулы и замкнутые классы отношений. Задачи обобщенной выполнимости S-ВЫП. Вычислительная сложность некоторых задач S-ВЫП.

Лекция 12. Функции на конечном множестве. Формулы и замкнутые классы функций. Сохранение отношения функцией, полиморфизмы. Двузначный случай.

Коллоквиум 3.

==Семинары==

Занятие 1. Сокращенная КНФ и способы ее построения.

Занятие 2. Полином Жегалкина. ЛКНФ и представимость в виде ЛКНФ.

Занятие 3. Классы P и NP, NP-полнота.

Коллоквиум 1 по теме "Функции алгебры логики и сложностные классы".

Занятие 4. Слабо положительные и слабо отрицательные функции.

Занятие 5. Биюнктивные и мультиаффинные функции.

Занятие 6. Теорема разделимости Шефера.

Коллоквиум 2 по теме "Теорема Шефера".


==Программа курса==

*Функции алгебры логики. Конъюнктивные и дизъюнктивные нормальные формы (КНФ и ДНФ). Сокращенная КНФ и способы ее построения. Полиномы Жегалкина, быстрый способ построения полинома Жегалкина функции. Линейные конъюнктивные нормальные формы (ЛКНФ). Проверка представимости функции в виде ЛКНФ.

*Задачи распознавания свойств. Классы P и NP. Полиномиальные, NP-трудные и NP-полные задачи. NP-полнота задачи k-раскраски графов при k >= 3. Задача обобщенной выполнимости S-ВЫП.

*Слабо положительные, слабо отрицательные и биюнктивные КНФ и слабо положительные, слабо отрицательные и биюнктивные функции алгебры логики. Критерии слабой положительности, слабой отрицательности и биюнктивности функции. Полиномиальность распознавания выполнимости слабо положительной, слабо отрицательной и биюнктивной КНФ.

*Линейные и мультиаффинные функции алгебры логики. Приведенное представление мультиаффинной функции алгебры логики. Критерий мультиаффинности функции. Полиномиальность распознавания выполнимости конъюнкции приведенных представлений мультиаффинных функций.

*Условная выразимость функций алгебры логики, леммы об условной выразимости функций (о транзитивности, о замене множителя в конъюнктивной форме, о подстановке констант вместо переменных и о навешивании отрицаний над переменными). Лемма о функции, сохраняющей константу 0, и функции, не сохраняющей константу 1. Лемма о функции, не являющейся самодополнительной. Лемма о функции, не являющейся слабо положительной, и функции, не являющейся слабо отрицательной. Леммы о небиюнктивной функции и немультиаффинной функции. Теорема Шефера о разделимости вычислительной сложности задачи S-ВЫП.

*Отношения на конечном множестве. Формулы, S-формулы и замкнутые классы отношений. Задача обобщенной выполнимости S-ВЫП. Функции на конечном множестве. Формулы и замкнутые классы функций. Сохранение отношения функцией, полиморфизмы. Двузначный случай.

==Экзамен==

Дискретные функции и выполнимость ограничений

2025-08-25T16:53:11Z

Root: Root переименовал страницу Дискретные функции и выполнимость ограничений в Обобщенная выполнимость

#перенаправление [[Обобщенная выполнимость]]

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

2025-05-13T10:03:49Z

Root:

#перенаправление [[Участник:ZakharovVA]]
[[Категория:Сотрудники кафедры математической кибернетики (архив)]]

Участник:ZakharovVA

2025-05-13T10:02:55Z

Root:

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

<div style="background-color: #FFAAAA; border-style: dotted">
'''Актуальность информации: 2022 год.'''

'''В настоящее время не является сотрудником кафедры.'''
</div>

[[Image:Zakharov.jpg|thumb|right|Захаров Владимир Анатольевич]]'''Захаров Владимир Анатольевич''' — доктор физико-математических наук, профессор кафедры МК.

email: zakh@cs.msu.su

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

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

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

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

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

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

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

=== Программно конфигурируемые сети ===
Программно-коммутируемые сети (ПКС) --- это класс компьютерных телекоммуникационных сетей, появившийся несколько лет назад в стремлении упростить проектирование и повысить гибкость управления сетями за счет разделения потоков данных (пакетов) и потоков управления (сообщений и команд), циркулирующие в сетях. ПКС представляет собой распределенную систему, в которой один или несколько контроллеров управляют множеством сетевых коммутаторов, обеспечивающих продвижение пакетов по каналам сети. Функциональные возможности и порядок взаимодействия коммутаторов и контроллеров ПКС определяются протоколом OpenFlow. Конструируются и исследуются формальные модели ПКС, разрабатываются методы и алгоритмы решения задач верификации и реконфигурации ПКС.

=== Информационная безопасность облачных вычислений ===
Исследуются вопросы о криптографической стойкости облачных вычислений над конфиденциальными данными. Для информационной защиты облачных вычислений могут быть использованы гомоморфные криптосистемы (в т.ч. пороговые). Исследуется также взаимосвязь между задачами обеспечения информационной безопасности облачных вычислений и обфускацией программ.

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

* [[Математическая логика и теория алгоритмов]] ((3 семестр))
* [[Математическая логика и логическое программирование (3-й поток)]] (7 семестр)
* [[Модели вычислений]] (8 семестр)
* [[Распределенные алгоритмы]] (10 семестр)
* [[Математические методы верификации схем и программ]] (11 семестр)
* [[Модели последовательных и параллельных вычислений]] (12 семестр)

== Спецсеминары ==
* [[Теоретические проблемы программирования ‎]]
* [[Некоторые вопросы теории управляющих систем ]]

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


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

'''Статьи в журналах'''

2017 [[О дедуктивной безопасности запросов к базам конфиденциальных данных в системе облачных вычислений]]

Варновский Н.П., Захаров В.А., Шокуров А.В.
в журнале ''Вестник Московского университета. Серия 15: Вычислительная математика и кибернетика, издательство Изд-во Моск. ун-та (М.), № 1, с. 38-44''

2016 [[On the minimization and equivalence checking of sequential reactive systems]]

Zakharov V.A., Temerbekova G.G.
в журнале ''Системная информатика, № 7, с. 33-44''

2016 [[К вопросу о существовании доказуемо стойких систем облачных вычислений]]

Варновский Н.П., Захаров В.А., Шокуров А.В.
в журнале ''Вестник Московского университета. Серия 15: Вычислительная математика и кибернетика, издательство Изд-во Моск. ун-та (М.), № 2, с. 32-38''

2016 [[О минимизации конечных автоматов-преобразователей над полугруппами]]

Захаров В.А., Темербекова Г.Г.
в журнале ''Моделирование и анализ информационных систем, издательство Яросл. гос. ун-т (Ярославль), том 23, № 6, с. 741-753''

2015 [[VERMONT - средство верификации программно-конфигурируемых сетей]]

Алтухов В.С., Захаров В.А., Подымов В.В., Чемерицкий Е.В.
в журнале ''Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Информатика. Телекоммуникации. Управление, том 212, № 1, с. 74-87''

2015 [[Комбинированное средство верификации распределённых вычислительных систем реального времени]]

Волканов Д.Ю., Захаров В.А., Зорин Д.А., Коннов И.В., Подымов В.В.
в журнале ''Программирование, № 6, с. 72-86''

2015 [[Моделирование и анализ поведения последовательных реагирующих программ]]

Захаров В.А.
в журнале ''Труды Института системного программирования РАН (электронный журнал), том 27, № 2, с. 221-250''

2015 [[Применение алгоритмов проверки эквивалентности для оптимизации программ]]

Захаров В.А., Подымов В.В.
в журнале ''Труды Института системного программирования РАН (электронный журнал), том 27, № 4, с. 145-174''

2014 [[О некоторых задачах реконфигурирования программно-конфигурируемых сетей]]

Захаров В.А., Чемерицкий Е.В.
в журнале ''Моделирование и анализ информационных систем, издательство Яросл. гос. ун-т (Ярославль), том 21, № 6, с. 57-69''

2014 [[Полиномиальный алгоритм проверки эквивалентности в модели программ с перестановочными и подавляемыми операторами]]

Подымов В.В., Захаров В.А.
в журнале ''Труды Института системного программирования РАН (электронный журнал), том 26, № 3, с. 145-166''

2014 [[Современное состояние исследований в области обфускации программ: определения стойкости обфускации]]

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В.
в журнале ''Труды Института системного программирования РАН (электронный журнал), том 26, № 3, с. 167-198''

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''

2010 [[Адаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времени]]

Захаров В.А., Коннов И.В. в журнале ''Моделирование и анализ информационных систем, том 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''

2007 [[Применение методов теории игр к поиску некоторых видов симуляции на размеченных системах переходов с ограничениями справедливости]]

Булычев П.Е., Захаров В.А. в журнале ''Вестник МЭИ, № 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''

1999 [[Быстрые алгоритмы разрешения эквивалентности пропозициональных операторных программ на упорядоченных полугрупповых шкалах]]

Захаров В.А. в журнале ''Вестник Московского университета. Серия 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''

'''Статьи в сборниках'''

2016 [[On the model checking of sequential reactive systems]]

Kozlova D., Zakharov V.
в сборнике ''Proceedings of the 25th International Workshop on Concurrency, Specification and Programming (CS&P 2016), серия CEUR Workshop Proceedings, издательство Humboldt Universitet Zu Berlin (Berlin, Germany), том 1698, с. 233-244''

2016 [[К вопросу о дедуктивной безопасности вычислений над зашифрованными данными]]
Варновский Н.П., Захаров В.А., Шокуров А.В.
в сборнике ''Материалы XII Международного семинара «Дискретная математика и ее приложения» имени академика О. Б. Лупанова (Москва, МГУ, 20–25 июня 2016 г.), место издания Изд-во механико-математического факультета МГУ Москва, с. 371-373''

2016 [[О проблеме логико-термальной эквивалентности недетерминированных стандартных схем программ]]
Захаров В.А., Попеско У.В.

в сборнике ''Материалы XII Международного семинара «Дискретная математика и ее приложения» имени академика О. Б. Лупанова (Москва, МГУ, 20–25 июня 2016 г.), место издания Изд-во механико-математического факультета МГУ Москва, с. 196-198''

2016 [[О проверке k-значности конечных автоматов-преобразователей над полугруппами]]

Джусупекова З.А., Захаров В.А.
в сборнике ''Материалы XII Международного семинара «Дискретная ма- тематика и ее приложения» имени академика О. Б. Лупанова (Москва, МГУ, 20–25 июня 2016 г.), место издания Изд-во механико-математического факультета МГУ Москва, с. 190-192''

2016 [[Оптимизирующие преобразования потоковых программ]]

Темербекова Г.Г., Захаров В.А.
в сборнике ''Материалы XII Международного семинара «Дискретная математика и ее приложения» имени академика О. Б. Лупанова (Москва, МГУ, 20–25 июня 2016 г.), место издания Изд-во механико-математического факультета МГУ Москва, с. 232-234''

2016 [[Темпоральная логика для верификации автоматов-преобразователей]]

Козлова Д.Г., Захаров В.А.
в сборнике ''Материалы XII Международного семинара «Дискретная математика и ее приложения» имени академика О. Б. Лупанова (Москва, МГУ, 20–25 июня 2016 г.), место издания Изд-во механико-математического факультета МГУ Москва, с. 204-206''

2015 [[Equivalence Checking Problem for Finite State Transducers]]

Zakharov V.A.
в сборнике ''Proceedings of the 6th International Conference on Algebraic Informatics, CAI 2015, Stuttgart, Germany, September 1-4, 2015, серия Lecture Notes in Computer Science, место издания Springer International Publishing Swirtzeland 2015 Swirtzeland, том 9270, с. 208-221''

2015 [[К вопросу о существовании доказуемо стойких систем облачных вычислений]]

Варновский Н.П., Захаров В.А., Шокуров А.В.
в сборнике ''Дискретные модели в теории управляющих систем. IX Международная конференция, Москва и Подмосковье, 20-22 мая 2015 г, серия ISBN 978-5-317-04970-6, место издания МАКС Пресс Москва, с. 50-52''

2015 [[Логико-термальная эквивалентность программ с динамической памятью]]

Новикова Т.А., Захаров В.А.
в сборнике ''Дискретные модели в теории управляющих систем. IX Международная конференция, Москва и Подмосковье, 20-22 мая 2015 г, серия ISBN 978-5-317-04970-6, место издания МАКС Пресс Москва, с. 173-176''

2014 [[A runtime verification system for Software Defined Networks]]

Altukhov V.S., Chemeritskiy E.V., Podymov V.V., Zakharov V.A.
в сборнике ''Материалы Международной научно-практической конференции: Tools & Methods of Program Analysis, TMPA-2014, место издания Кострома: КГТУ, с. 19-28''

2014 [[Consistent network update without tagging]]

Chemeritskiy E.V., Zakharov V.A.
в сборнике ''SDN&NFV:The Next Generation of Comput. Infrastructure: 2014 Intern. Sci. and Technol. Conf. "Modern Networking Technologies (MoNeTec)", место издания МАКС Пресс Москва, с. 47-52''

2014 [[VERMONT - a toolset for checking SDN packet forwarding policies on-line]]

Altukhov V.S., Chemeritskiy E.V., Podymov V.V., Zakharov V.A.
в сборнике ''SDN and NFV: Next Generation of Computational Infrastructure - 2014 International Science and Technology Conference - Modern Networking Technologies, MoNeTec 2014, Proceedings, место издания МАКС Пресс Москва, с. 7-12''

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''

2013 [[An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts]]

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''

2013 [[DYANA: an integrated development environment for simulation and verification of real-time avionics systems]]

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''

2007 [[On the verification of asynchronous parameterized networks of communicating processes by model checking]]

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''

2006 [[Об особенностях применения методов обфускации программ для информационной защиты микроэлектронных схем]]

Варновский Н.П., Захаров В.А., Кузюрин Н.Н., Шокуров А.В., Чернов А.В.
в сборнике ''Труды Института Системного программирования, место издания ИСП РАН, том 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''

2005 [[О возможности применения быстрых алгоритмов проверки эквивалентности программ для обнаружения вирусов]]

Захаров В.А., Захарьящев И.М., Подловченко Р.И., Русаков Д.М., Щербина В.Л.
в сборнике ''Труды второй всероссийской конференции «Методы и средства обработки информации», место издания Изд-во ф-та ВМК МГУ Москва, с. 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''

2000 [[Общие методы построения разрешающих алгоритмов эквивалентности пропозициональных операторных программ]]

Захаров В.А.
в сборнике ''Труды 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''

1998 [[An efficient and unified approach to the decidability of equivalence of propositional program schemes]]

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

Зизов Вадим Сергеевич

2025-05-13T10:01:06Z

Root: Перенаправление на Участник:ZizovVS

#REDIRECT [[Участник:ZizovVS]]
[[Категория:Сотрудники лаборатории ДУСП]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

Участник:ZizovVS

2025-05-13T10:01:02Z

Root:

{{DISPLAYTITLE:Зизов Вадим Сергеевич}}
[[Image:Zizov.jpg|thumb|right|Зизов Вадим Сергеевич]]'''Зизов Вадим Сергеевич''' — младший научный сотрудник кафедры МК.

* e-mail: vzs815@gmail.com
* [http://istina.msu.ru/profile/alvadia/ Профиль в системе ИСТИНА]

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

==Вложение графов и структурное моделирование в некоторых моделях вычислений==

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

= Семинарские занятия =

* [[Математическая логика (группы 318, 241)]]
* [[Основы кибернетики (2-й поток, 3 курс)]]
* [[Основы кибернетики (3-й поток)]]
* [[Дискретная математика (2-й поток)]]
* Практикум на ЭВМ

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

* [[Теория управляющих систем и математические модели СБИС]]

= Спецкурсы =
* [[Геометрическая реализация графов и схем]]

Андреева Татьяна Владимировна

2025-04-25T10:46:56Z

Root: Перенаправление на Участник:AndreevaTV

#перенаправление [[Участник:AndreevaTV]]
[[Категория:Сотрудники кафедры математической кибернетики]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

Участник:AndreevaTV

2025-04-25T10:46:03Z

Root: Новая страница: «{{DISPLAYTITLE:Андреева Татьяна Владимировна}} '''Андреева Татьяна Владимировна''' — кандидат фи…»

{{DISPLAYTITLE:Андреева Татьяна Владимировна}}
'''Андреева Татьяна Владимировна''' — кандидат физико-математических наук, старший преподаватель кафедры МК.

Дискретная математика (1й курс)

2025-01-29T14:21:38Z

Root: Root переименовал страницу Дискретная математика (1й курс) в Дискретная математика (1-й курс)

#перенаправление [[Дискретная математика (1-й курс)]]

Дискретная математика (1-й курс)

2025-01-29T14:21:38Z

Root: Root переименовал страницу Дискретная математика (1й курс) в Дискретная математика (1-й курс)

[[Категория:Лекционные курсы кафедры МК]]

== Лекторы ==
*проф. [[Алексеев Валерий Борисович| Алексеев Валерий Борисович]]
*проф. [[Марченков Сергей Серафимович| Марченков Сергей Серафимович]]
*проф. [[Селезнева Светлана Николаевна| Селезнева Светлана Николаевна]]

== Экзамен 2024. Вопросы к экзамену по курсу «Дискретная математика» для 2 и 3 потоков, 2024 год.==

Экзамен планируется устный. В билете 2 вопроса (один из части А и один из части В) и задача.

===Часть А===
Часть А – ответ без подготовки, по любым материалам (конспекты, книжки, распечатки лекций и т.д.). Можно смотреть текст на ноутбуке, но нельзя пользоваться мобильными телефонами. Проверяется, насколько осознаны все доказательства (основной вопрос – «почему?»). Определения и формулировки – без конспектов.
<ol>
<li> Алгоритм построения вектора коэффициентов полинома Жегалкина (с обоснованием).
<li> Двойственность. Класс самодвойственных функций, его замкнутость.
<li> Лемма о нелинейной функции.
<li> Теорема Поста о полноте системы функций алгебры логики.
<li> Теорема о предполных классах.
<li> Деревья. Свойства деревьев.
<li> Алгоритм построения кратчайшего остовного дерева (с обоснованием).
<li> Теорема о раскраске планарных графов в 5 цветов.
<li> Алгоритм распознавания взаимной однозначности алфавитного кодирования (с обоснованием).
<li> Теорема Маркова.
<li> Неравенство Макмиллана.
<li> Существование префиксного кода с заданными длинами кодовых слов.
<li> Теорема редукции.
<li> Коды с исправлением r ошибок. Оценка функции Mr(n).
<li> Коды Хэмминга. Оценка функции M1(n).
<li> Схемы из функциональных элементов и элементов задержки. Автоматность осуществляемых ими отображений.
<li> Моделирование автоматной функции схемой из функциональных элементов и элементов задержки.
<li> Теорема Мура.
<li> Метод Карацубы построения схемы для умножения, верхняя оценка ее сложности.
</ol>

=== Часть В ===
Часть В – ответ без конспектов и других материалов и почти без подготовки (3-5 минут), с доказательствами (можно излагать устно).
<ol start="20">
<li> Функции алгебры логики. Равенство функций. Тождества для элементарных функций.
<li> Теорема о разложении функции алгебры логики по переменным. Теорема о совершенной дизъюнктивной нормальной форме.
<li> Полные системы. Примеры полных систем (с доказательством полноты).
<li> Теорема Жегалкина о представимости функции алгебры логики полиномом.
<li> Понятие замкнутого класса. Замкнутость классов T0, T1, L.
<li> Класс монотонных функций, его замкнутость.
<li> Лемма о несамодвойственной функции.
<li> Лемма о немонотонной функции.
<li> Теорема о максимальном числе функций в базисе в алгебре логики.
<li> Основные понятия теории графов. Изоморфизм графов. Связность.
<li> Корневые деревья. Верхняя оценка их числа.
<li> Геометрическая реализация графов. Теорема о реализации графов в трехмерном пространстве.
<li> Планарные (плоские) графы. Формула Эйлера.
<li> Доказательство непланарности графов K5 и K3,3. Теорема Понтрягина-Куратовского (доказательство в одну сторону).
<li> Теорема о раскраске вершин графа в 2 цвета (теорема Кенига).
<li> Оптимальные коды, их свойства.
<li> Линейные двоичные коды. Теорема о кодовом расстоянии линейных кодов.
<li> Схемы из функциональных элементов. Реализация функций алгебры логики схемами.
<li> Сумматор. Верхняя оценка сложности сумматора. Вычитатель.
<li> Понятие автоматных функций, их представление диаграммой Мура. Единичная задержка.
</ol>
Третьим пунктом в билете стоит задача по одной из 4 тем: алгебра логики, графы, коды, автоматы.
Задачи решаются без конспектов и любых других материалов.

После ответа на билет возможна прогонка по всему материалу без конспекта (определения, формулировки, идеи доказательств) и добавочные задачи на любые темы.

===Литература===
<ol>
<li> Собственный конспект лекций.
<li> Лекции (онлайн) Алексеева В.Б. по дискретной математике: https://www.youtube.com/watch?v=SAhzEOVDNEI&list=PLcsjsqLLSfNAY-pm5c4XZQhSl1U_20itT
<li> Алексеев В.Б. Лекции по дискретной математике. М.: Инфра-М, 2012. (Вопросы 2-6, 8-33, 35, 37-39)
<li> [[Media:Lectdm.pdf|Алексеев В.Б. Лекции по дискретной математике. ВМК, 2004.]] Электронный ресурс. (Вопросы 2-6, 8-33, 35, 37-39)
<li> Яблонский С.В. Введение в дискретную математику. М.: Наука, 1986. (Вопросы 2-5, 10-12, 20-28)
<li> Гаврилов Г.П., Сапоженко А.А. Задачи и упражнения по дискретной математике. М.: Физматлит, 2004. (Вопрос 1 (стр. 53-56) и вопрос 36 (задача 4.9 из главы 7))
<li> [[Media:KNIGA1.pdf|Алексеев В.Б. Введение в теорию сложности алгоритмов.]] М.: Издательский отдел факультета ВМК МГУ, 2002 (Вопрос 7)
<li> Емеличев В.А., Мельников О.И., Сарванов В.И., Тышкевич Р.И. Лекции по теории графов. М.: Наука, 1990 (Вопрос 34 (стр. 36-37 и 237))
<li> Весь материал имеется также в книге: Алексеев В.Б. Дискретная математика : учебник. М.: Инфра-М, 2021 (доступна в электронной библиотечной системе (ЭБС) Znanium.com).
</ol>

Марченков Сергей Серафимович

2024-10-21T17:04:27Z

Root:

#перенаправление [[Участник:MarchenkovSS]]

Участник:MarchenkovSS

2024-10-21T17:03:47Z

Root:

<div style="background-color: #FFAAAA; border-style: dotted">
'''Актуальность информации: 2024 год.'''

'''В настоящее время не является сотрудником кафедры.'''
</div>

{{DISPLAYTITLE:Марченков Сергей Серафимович}}
[[Image:Marchenkov.jpg|thumb|right|Марченков Сергей Серафимович]]'''Марченков Сергей Серафимович''' — доктор физико-математических наук, профессор кафедры МК.

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

=== Теория функциональных систем ===

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

=== Теория алгоритмов ===

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

=== Теория автоматов ===

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

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

* [[Дискретная математика (1й курс)]]
* [[Дополнительные главы дискретной математики (2-й поток III курса) ]]
* [[Однородные функции]]
* [[Операторы замыкания в многозначной логике]]
* [[Основы теории алгоритмов]]
* [[Предикатное определение замкнутых классов]]
* [[Предполные классы многозначной логики]]
* [[Частичные булевы функции]]
* [[Элементарные рекурсивные функции]]

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

* [[Дискретные функции и сложность алгоритмов ]]

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

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

# Об одном классе неполных множеств // Математические заметки. - 1976. - Т. 20, N 4. - C. 473-478.
# Об одном методе анализа суперпозиций непрерывных функций // Проблемы кибернетики, вып. 37. - 1980. - С. 5-17.
# Однородные алгебры // Проблемы кибернетики, вып. 39. - 1982. - С. 85-106.
# Классификация алгебр со знакопеременной группой автоморфизмов // Математические вопросы кибернетики, вып. 2. - 1989. - С. 100-122.
# Конечные начальные сегменты верхней полурешетки конечно-автоматных степеней // Дискретная математика. - 1989. - Т. 1, N 3. - C. 96-103.
# Простые примеры базисов по суперпозиции в классе функций, элементарных по Кальмару // Banach Center Publication. - 1989. - V. 25. - P. 119-126.
# О представлении словарных предикатов из арифметической иерархии // Дискретная математика. - 1990. - Т. 2, N 1. - C. 87-93.
# О равномерном id-разложении булевых функций // Дискретная математика. - 1990. - Т. 2, N 3. - C. 29-41.
# Базисы по суперпозиции в классах рекурсивных функций // Математические вопросы кибернетики, вып. 3. - 1991. - С. 115-139.
# О классах Слупецкого в системах P_k...P_l// Дискретная математика. - 1992. - Т. 4, N 3. - C. 135-148.
# Предполнота замкнутых классов в P_k: предикатный подход // Математические вопросы кибернетики, вып. 6. - 1996. - С. 117-132.
# S-классификация функций многозначной логики // Дискретная математика. - 1997. - Т. 9, N 3. - С. 125-152.
# Инварианты классов Поста // Фундаментальная и прикладная математика. - 1998. - Т. 4, N 4. - С. 1385-1404.
# A-классификация идемпотентных функций многозначной логики // Дискретный анализ и исследование операций. Серия 1. - 1999. - Т. 6, N 1. - С. 19-43.
# О суперпозициях непрерывных функций, заданных на бэровском пространтстве // Математические заметки. - 1999. - Т. 66, N 5. - С. 696-705.
# Замкнутые классы булевых функций. // М.: Наука, 2000, 126 стр.
# О невозможности получения (n+1)-местных непрерывных функций из n-местных с помощью некоторых непрерывных операторов. // Математический сборник. - 2001. - Т. 192, N 6. - С. 71-88.
# S-классификация функций трехзначной логики. // М.:Физматлит. 2001, 80 стр
# Элементарные рекурсивные функции. // М.: МЦНМО, 2003, 112 стр.
# О сложности возвратных последовательностей. // Дискретная математика. - 2003. - Т. 15, Т 2. - С. 52-62.

Файл:MLLP VP 19.pdf

2023-10-11T12:21:48Z

Root: Root загружена новая версия «Файл:MLLP VP 19.pdf»

Мат. лог. и лог. прог., 3 поток. Блок 19. Системы дизъюнктов

Распределенные алгоритмы и системы

2023-08-29T10:48:12Z

Root:

[[Категория:Лекционные курсы кафедры МК]]

Обязательный курс для студентов группы 521. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].

Актуальность информации: весенний семестр 2022/2023 учебного года.

= Слайды лекций =

[[Media: DAS_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.

[[Media: DAS_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.

[[Media: DAS_VP_03.pdf| Блок 3.]] Модель распределённой системы: система переходов системы, система переходов узла, распределённый алгоритм, асинхронный и синхронный обмен сообщениями.

[[Media: DAS_VP_04.pdf| Блок 4.]] Справедливые вычисления.

[[Media: DAS_VP_05.pdf| Блок 5.]] Иллюстрация трудности разработки распределённых алгоритмов

[[Media: DAS_VP_06.pdf| Блок 6.]] Причинно-следственный порядок событий.

[[Media: DAS_VP_07.pdf| Блок 7.]] Логические часы.

[[Media: DAS_VP_08.pdf| Блок 8.]] Дополнительные допущения. Сложность.

[[Media: DAS_VP_09.pdf| Блок 9.]] Симметричный протокол раздвижного окна.

[[Media: DAS_VP_10.pdf| Блок 10.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости.

[[Media: DAS_VP_11.pdf| Блок 11.]] Корректность симметричного протокола раздвижного окна.

[[Media: DAS_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна.

[[Media: DAS_VP_13.pdf| Блок 13.]] Коммуникационный протокол с таймерами.

[[Media: DAS_VP_14.pdf| Блок 14.]] Корректность протокола с таймерами.

[[Media: DAS_VP_15.pdf| Блок 15.]] Задача маршрутизации.

[[Media: DAS_VP_16.pdf| Блок 16.]] Основные допущения о весах в задаче маршрутизации. Маршрутизация и свойства графов.

[[Media: DAS_VP_17.pdf| Блок 17.]] Построение оптимальных путей для всех пар вершин. Алгоритм Флойда-Уоршелла.

[[Media: DAS_VP_18.pdf| Блок 18.]] Алгоритм маршрутизации Туэга.

[[Media: DAS_VP_19.pdf| Блок 19.]] Алгоритм маршрутизации Мерлина-Сигалла.

[[Media: DAS_VP_20.pdf| Блок 20.]] Алгоритм маршрутизации Чанди-Мисры.

[[Media: DAS_VP_21.pdf| Блок 21.]] Волновые алгоритмы: основные определения и свойства.

[[Media: DAS_VP_22.pdf| Блок 22.]] Применение волновых алгоритмов: PIF, SYN, INF.

[[Media: DAS_VP_23.pdf| Блок 23.]] Примеры волновых алгоритмов: кольцевой алгоритм, древесный алгоритм, алгоритм эха.

[[Media: DAS_VP_24.pdf| Блок 24.]] Примеры волновых алгоритмов: фазовый алгоритм.

[[Media: DAS_VP_25.pdf| Блок 25.]] Примеры волновых алгоритмов: алгоритм Финна.

[[Media: DAS_VP_26.pdf| Блок 26.]] Распределённые алгоритмы обхода. Алгоритм Тарри. Классический распределённый обход в глубину.

[[Media: DAS_VP_27.pdf| Блок 27.]] Распределённый обход в глубину: алгоритм Авербаха.

[[Media: DAS_VP_28.pdf| Блок 28.]] Алгоритмы избрания лидера: основные определения и допущения, волновое избрание лидера.

[[Media: DAS_VP_29.pdf| Блок 29.]] Избрание лидера в дереве.

[[Media: DAS_VP_30.pdf| Блок 30.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.

[[Media: DAS_VP_31.pdf| Блок 31.]] Избрание лидера: эффект угасания.

[[Media: DAS_VP_32.pdf| Блок 32.]] Избрание лидера: нижние оценки.

[[Media: DAS_VP_33.pdf| Блок 33.]] Избрание лидера: алгоритм Галладжера-Хамблета-Спиры (GHS).

[[Media: DAS_VP_34.pdf| Блок 34.]] Задача сохранения снимка сети.

[[Media: DAS_VP_35.pdf| Блок 35.]] Сохранение снимка сети: алгоритм Чанди-Лэмпорта.

[[Media: DAS_VP_36.pdf| Блок 36.]] Сохранение снимка сети: алгоритм Лаи-Янга.

[[Media: DAS_VP_37.pdf| Блок 37.]] Задача обнаружения завершения вычислений.

[[Media: DAS_VP_38.pdf| Блок 38.]] Обнаружение завершения вычислений: алгоритм Дейкстры-Шолтена.

[[Media: DAS_VP_39.pdf| Блок 39.]] Обнаружение завершения вычислений: алгоритм Шави-Франчеза.

[[Media: DAS_VP_40.pdf| Блок 40.]] Обнаружение завершения вычислений: алгоритм возвращения кредита.

[[Media: DAS_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи принятия решения.

[[Media: DAS_VP_42.pdf| Блок 42.]] Задача консенсуса.

[[Media: DAS_VP_43.pdf| Блок 43.]] Консенсус: Паксос.

''Слайды будут появляться по мере проведения занятий''

== Прошлогодние слайды ==

[[Media: Lecture-DA-1.pdf| Lecture 1]].
[[Media: Lecture-DA-2.pdf| Lecture 2]].
[[Media: Lecture-DA-3.pdf| Lecture 3]].
[[Media: Lecture-DA-4.pdf| Lecture 4]].
[[Media: Lecture-DA-5.pdf| Lecture 5]].
[[Media: Lecture-DA-6.pdf| Lecture 6]].
[[Media: Lecture-DA-7.pdf| Lecture 7]].
[[Media: Lecture-DA-8.pdf| Lecture 8]].
[[Media: Lecture-DA-9.pdf| Lecture 9]].
[[Media: Lecture-DA-10.pdf| Lecture 10]].
[[Media: Lecture-DA-11.pdf| Lecture 11]].
[[Media: Lecture-DA-12.pdf| Lecture 12]].

= Литература =

#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.

Распределенные алгоритмы и системы

2023-08-29T10:47:59Z

Root: Root переименовал страницу Распределенные алгоритмы в Распределенные алгоритмы и системы: Актуальное название

Обязательный курс для студентов группы 521. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].

Актуальность информации: весенний семестр 2022/2023 учебного года.

= Слайды лекций =

[[Media: DAS_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.

[[Media: DAS_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.

[[Media: DAS_VP_03.pdf| Блок 3.]] Модель распределённой системы: система переходов системы, система переходов узла, распределённый алгоритм, асинхронный и синхронный обмен сообщениями.

[[Media: DAS_VP_04.pdf| Блок 4.]] Справедливые вычисления.

[[Media: DAS_VP_05.pdf| Блок 5.]] Иллюстрация трудности разработки распределённых алгоритмов

[[Media: DAS_VP_06.pdf| Блок 6.]] Причинно-следственный порядок событий.

[[Media: DAS_VP_07.pdf| Блок 7.]] Логические часы.

[[Media: DAS_VP_08.pdf| Блок 8.]] Дополнительные допущения. Сложность.

[[Media: DAS_VP_09.pdf| Блок 9.]] Симметричный протокол раздвижного окна.

[[Media: DAS_VP_10.pdf| Блок 10.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости.

[[Media: DAS_VP_11.pdf| Блок 11.]] Корректность симметричного протокола раздвижного окна.

[[Media: DAS_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна.

[[Media: DAS_VP_13.pdf| Блок 13.]] Коммуникационный протокол с таймерами.

[[Media: DAS_VP_14.pdf| Блок 14.]] Корректность протокола с таймерами.

[[Media: DAS_VP_15.pdf| Блок 15.]] Задача маршрутизации.

[[Media: DAS_VP_16.pdf| Блок 16.]] Основные допущения о весах в задаче маршрутизации. Маршрутизация и свойства графов.

[[Media: DAS_VP_17.pdf| Блок 17.]] Построение оптимальных путей для всех пар вершин. Алгоритм Флойда-Уоршелла.

[[Media: DAS_VP_18.pdf| Блок 18.]] Алгоритм маршрутизации Туэга.

[[Media: DAS_VP_19.pdf| Блок 19.]] Алгоритм маршрутизации Мерлина-Сигалла.

[[Media: DAS_VP_20.pdf| Блок 20.]] Алгоритм маршрутизации Чанди-Мисры.

[[Media: DAS_VP_21.pdf| Блок 21.]] Волновые алгоритмы: основные определения и свойства.

[[Media: DAS_VP_22.pdf| Блок 22.]] Применение волновых алгоритмов: PIF, SYN, INF.

[[Media: DAS_VP_23.pdf| Блок 23.]] Примеры волновых алгоритмов: кольцевой алгоритм, древесный алгоритм, алгоритм эха.

[[Media: DAS_VP_24.pdf| Блок 24.]] Примеры волновых алгоритмов: фазовый алгоритм.

[[Media: DAS_VP_25.pdf| Блок 25.]] Примеры волновых алгоритмов: алгоритм Финна.

[[Media: DAS_VP_26.pdf| Блок 26.]] Распределённые алгоритмы обхода. Алгоритм Тарри. Классический распределённый обход в глубину.

[[Media: DAS_VP_27.pdf| Блок 27.]] Распределённый обход в глубину: алгоритм Авербаха.

[[Media: DAS_VP_28.pdf| Блок 28.]] Алгоритмы избрания лидера: основные определения и допущения, волновое избрание лидера.

[[Media: DAS_VP_29.pdf| Блок 29.]] Избрание лидера в дереве.

[[Media: DAS_VP_30.pdf| Блок 30.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.

[[Media: DAS_VP_31.pdf| Блок 31.]] Избрание лидера: эффект угасания.

[[Media: DAS_VP_32.pdf| Блок 32.]] Избрание лидера: нижние оценки.

[[Media: DAS_VP_33.pdf| Блок 33.]] Избрание лидера: алгоритм Галладжера-Хамблета-Спиры (GHS).

[[Media: DAS_VP_34.pdf| Блок 34.]] Задача сохранения снимка сети.

[[Media: DAS_VP_35.pdf| Блок 35.]] Сохранение снимка сети: алгоритм Чанди-Лэмпорта.

[[Media: DAS_VP_36.pdf| Блок 36.]] Сохранение снимка сети: алгоритм Лаи-Янга.

[[Media: DAS_VP_37.pdf| Блок 37.]] Задача обнаружения завершения вычислений.

[[Media: DAS_VP_38.pdf| Блок 38.]] Обнаружение завершения вычислений: алгоритм Дейкстры-Шолтена.

[[Media: DAS_VP_39.pdf| Блок 39.]] Обнаружение завершения вычислений: алгоритм Шави-Франчеза.

[[Media: DAS_VP_40.pdf| Блок 40.]] Обнаружение завершения вычислений: алгоритм возвращения кредита.

[[Media: DAS_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи принятия решения.

[[Media: DAS_VP_42.pdf| Блок 42.]] Задача консенсуса.

[[Media: DAS_VP_43.pdf| Блок 43.]] Консенсус: Паксос.

''Слайды будут появляться по мере проведения занятий''

== Прошлогодние слайды ==

[[Media: Lecture-DA-1.pdf| Lecture 1]].
[[Media: Lecture-DA-2.pdf| Lecture 2]].
[[Media: Lecture-DA-3.pdf| Lecture 3]].
[[Media: Lecture-DA-4.pdf| Lecture 4]].
[[Media: Lecture-DA-5.pdf| Lecture 5]].
[[Media: Lecture-DA-6.pdf| Lecture 6]].
[[Media: Lecture-DA-7.pdf| Lecture 7]].
[[Media: Lecture-DA-8.pdf| Lecture 8]].
[[Media: Lecture-DA-9.pdf| Lecture 9]].
[[Media: Lecture-DA-10.pdf| Lecture 10]].
[[Media: Lecture-DA-11.pdf| Lecture 11]].
[[Media: Lecture-DA-12.pdf| Lecture 12]].

= Литература =

#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.

Распределенные алгоритмы

2023-08-29T10:47:59Z

#перенаправление [[Распределенные алгоритмы и системы]]

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

2023-08-29T10:46:38Z

Root:

[[Категория:Лекционные курсы кафедры МК]]

Обязательный курс для студентов групп 618/1 и 618/2. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].

Актуальность информации: весенний семестр 2022/2023 учебного года.

= Слайды лекций =

[[Media: MMSC_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.

[[Media: MMSC_VP_02.pdf| Блок 2.]] Сети Петри: происхождение, основные понятия.

[[Media: MMSC_VP_03.pdf| Блок 3.]] Сети Петри: примеры применения и свойства поведения.

[[Media: MMSC_VP_04.pdf| Блок 4.]] Проблемы ограниченности и безопасности сетей Петри. Деревья покрытия разметок.

[[Media: MMSC_VP_05.pdf| Блок 5.]] Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

[[Media: MMSC_VP_06.pdf| Блок 6.]] Проблемы достижимости и живости для сетей Петри.

[[Media: MMSC_VP_07.pdf| Блок 7.]] Диофантовы уравнения.

[[Media: MMSC_VP_08.pdf| Блок 8.]] Моделирование многочленов сетями Петри.

[[Media: MMSC_VP_09.pdf| Блок 9.]] Проблемы R-включения и R-эквивалентности для сетей Петри.

[[Media: MMSC_VP_10.pdf| Блок 10.]] Языки сетей Петри.

[[Media: MMSC_VP_11.pdf| Блок 11.]] Другие виды сетей Петри.

[[Media: MMSC_VP_12.pdf| Блок 12.]] Проблема эквивалентности программ. Схемы программ.

[[Media: MMSC_VP_13.pdf| Блок 13.]] Схемы Ляпунова-Янова.

[[Media: MMSC_VP_14.pdf| Блок 14.]] Стандартные схемы программ.

[[Media: MMSC_VP_15.pdf| Блок 15.]] Подстановки. Системы переходов стандартных схем программ.

[[Media: MMSC_VP_16.pdf| Блок 16.]] Проблемы функциональной эквивалентности, пустоты и свободы для стандартных схем программ.

[[Media: MMSC_VP_17.pdf| Блок 17.]] Двухголовочные автоматы.

[[Media: MMSC_VP_18.pdf| Блок 18.]] Эрбрановские интерпретации для стандартных схем программ.

[[Media: MMSC_VP_19.pdf| Блок 19.]] Неразрешимость основных проблем для стандартных схем программ

[[Media: MMSC_VP_20.pdf| Блок 20.]] Алгебра процессов. Базовая алгебра процессов (BPA).

[[Media: MMSC_VP_21.pdf| Блок 21.]] Алгебра процессов с параллелизмом (PAP).

[[Media: MMSC_VP_22.pdf| Блок 22.]] Алгебра взаимодействующих процессов (ACP).

[[Media: MMSC_VP_23.pdf| Блок 23.]] Бисимуляция процессов.

[[Media: MMSC_VP_24.pdf| Блок 24.]] Консервативные расширения систем процессов.

[[Media: MMSC_VP_25.pdf| Блок 25.]] Рекурсия в системах процессов.

''Слайды будут появляться по мере проведения занятий''

== Прошлогодние слайды ==

[[Media: Lecture_PM_1.pdf| Лекция 1]].
[[Media: Lecture_PM_2.pdf| Лекция 2]].
[[Media: Lecture_PM_3.pdf| Лекция 3]].
[[Media: Lecture_PM_4.pdf| Лекция 4]].
[[Media: Lecture_PM_5.pdf| Лекция 5]].
[[Media: Lecture_PM_6.pdf| Лекция 6]].
[[Media: Lecture_PM_7.pdf| Лекция 7]].
[[Media: Lecture_PM_8.pdf| Лекция 8]].
[[Media: Lecture_PM_9.pdf| Лекция 9]].

= Программа курса =

== Сети Петри ==
<ol>
<li> Сети позиций и переходов. Мультимножества и операции над ними. Разметки. Сети Петри.
<li> Условия срабатывания переходов. Отношение срабатывания переходов. Вычисления обыкновенных сетей Петри. Достижимые и тупиковые разметки. Граф достижимых разметок обыкновенной сети Петри.
<li> Сравнение разметок. Теорема о свойстве монотонности вычислений обыкновенных сетей Петри.
<li> Свойства ограниченности, безопасности и консервативности сетей Петри.
<li> Свойства живости и устойчивости сетей Петри.
<li> Проблемы достижимости и R-эквивалентности для сетей Петри.
<li> Моделирование многочленов обыкновенными сетями Петри. Неразрешимость проблемы R-эквивалентности для обыкновенных сетей Петри.
<li> Языки, порождаемые сетями Петри. Примеры языков, порождаемых сетями Петри. Сравнение класса языков, порождаемых обыкновенными сетями Петри, и классов языков иерархии Хомского.
<li> Ординарные сети Петри. Моделирование обыкновенных сетей Петри ординарными сетями.
<li> Автоматные сети Петри. Моделирование конечных автоматов автоматными сетями Петри.
<li> Синхронизационные сети Петри. Условия живости и консервативности для синхронизационных сетей Петри.
<li> Сети потоков работ.
<li> Ингибиторные сети Петри. Моделирование счетчиковых машин Минского ингибиторными сетями Петри.
<li> Раскрашенные сети Петри.
</ol>

== Схемы программ ==
<ol start="15">
<li> Проблема эквивалентности программ и трудности ее решения. Моделирование программ схемами программ.
<li> Стандартные схемы программ: синтаксис и семантика. Вычисления стандартных схем программ.
<li> Задачи анализа поведения стандартных схем программ - проблемы пустоты, эквивалентности, свободы схем программ.
<li> Представление стандартных схем программ при помощи систем переходов и алгебры подстановок.
<li> Эрбрановские интерпретации для стандартных схем программ. Эквивалентность стандартных схем программ на эрбрановских интерпретациях.
<li> Неразрешимость проблем анализа поведения стандартных схем программ.
<li> Схемы программ Ляпунова-Янова.
<li> Взаимосвязь схем программ Ляпунова-Янова и конечных автоматов. Разрешимость проблемы эквивалентности для схем Ляпунова-Янова.
</ol>

== Алгебра процессов ==
<ol start="23">
<li> Базовая алгебра процессов.
<li> Алгебра процессов с параллелизмом.
<li> Алгебра взаимодействующих процессов.
<li> Процессные графы.
<li> Бисимуляция процессов.
<li> Консервативное расширение алгебры процессов.
<li> Рекурсия в алгебре процессов.
</ol>

= Литература =

<ol>
<li> Котов В.Е. Сети Петри - М.: Мир, 1984.
<li> Питерсон Дж. Теория сетей Петри и моделирование систем. - М.: Мир, 1984.
<li> Ломазова И.А. Вложенные сети Петри: моделирование м анализ распределенных систем с объектной структурой - М.: Научный мир, 2004.
<li> Reisig W. Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. - Springer, 2013.
<li> Котов В.Е., Сабельфельд В.К. Теория схем программ - М.: Мир, 1983.
<li> Fokkink W. Introduction to process algebra. Springer Berlin, Heidelberg, 2000
</ol>

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

2023-08-29T10:46:20Z

Root: Root переименовал страницу Модели последовательных и параллельных вычислений в Математические модели последовательных вычислений: А…

Обязательный курс для студентов групп 618/1 и 618/2. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].

Актуальность информации: весенний семестр 2022/2023 учебного года.

= Слайды лекций =

[[Media: MMSC_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.

[[Media: MMSC_VP_02.pdf| Блок 2.]] Сети Петри: происхождение, основные понятия.

[[Media: MMSC_VP_03.pdf| Блок 3.]] Сети Петри: примеры применения и свойства поведения.

[[Media: MMSC_VP_04.pdf| Блок 4.]] Проблемы ограниченности и безопасности сетей Петри. Деревья покрытия разметок.

[[Media: MMSC_VP_05.pdf| Блок 5.]] Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

[[Media: MMSC_VP_06.pdf| Блок 6.]] Проблемы достижимости и живости для сетей Петри.

[[Media: MMSC_VP_07.pdf| Блок 7.]] Диофантовы уравнения.

[[Media: MMSC_VP_08.pdf| Блок 8.]] Моделирование многочленов сетями Петри.

[[Media: MMSC_VP_09.pdf| Блок 9.]] Проблемы R-включения и R-эквивалентности для сетей Петри.

[[Media: MMSC_VP_10.pdf| Блок 10.]] Языки сетей Петри.

[[Media: MMSC_VP_11.pdf| Блок 11.]] Другие виды сетей Петри.

[[Media: MMSC_VP_12.pdf| Блок 12.]] Проблема эквивалентности программ. Схемы программ.

[[Media: MMSC_VP_13.pdf| Блок 13.]] Схемы Ляпунова-Янова.

[[Media: MMSC_VP_14.pdf| Блок 14.]] Стандартные схемы программ.

[[Media: MMSC_VP_15.pdf| Блок 15.]] Подстановки. Системы переходов стандартных схем программ.

[[Media: MMSC_VP_16.pdf| Блок 16.]] Проблемы функциональной эквивалентности, пустоты и свободы для стандартных схем программ.

[[Media: MMSC_VP_17.pdf| Блок 17.]] Двухголовочные автоматы.

[[Media: MMSC_VP_18.pdf| Блок 18.]] Эрбрановские интерпретации для стандартных схем программ.

[[Media: MMSC_VP_19.pdf| Блок 19.]] Неразрешимость основных проблем для стандартных схем программ

[[Media: MMSC_VP_20.pdf| Блок 20.]] Алгебра процессов. Базовая алгебра процессов (BPA).

[[Media: MMSC_VP_21.pdf| Блок 21.]] Алгебра процессов с параллелизмом (PAP).

[[Media: MMSC_VP_22.pdf| Блок 22.]] Алгебра взаимодействующих процессов (ACP).

[[Media: MMSC_VP_23.pdf| Блок 23.]] Бисимуляция процессов.

[[Media: MMSC_VP_24.pdf| Блок 24.]] Консервативные расширения систем процессов.

[[Media: MMSC_VP_25.pdf| Блок 25.]] Рекурсия в системах процессов.

''Слайды будут появляться по мере проведения занятий''

== Прошлогодние слайды ==

[[Media: Lecture_PM_1.pdf| Лекция 1]].
[[Media: Lecture_PM_2.pdf| Лекция 2]].
[[Media: Lecture_PM_3.pdf| Лекция 3]].
[[Media: Lecture_PM_4.pdf| Лекция 4]].
[[Media: Lecture_PM_5.pdf| Лекция 5]].
[[Media: Lecture_PM_6.pdf| Лекция 6]].
[[Media: Lecture_PM_7.pdf| Лекция 7]].
[[Media: Lecture_PM_8.pdf| Лекция 8]].
[[Media: Lecture_PM_9.pdf| Лекция 9]].

= Программа курса =

== Сети Петри ==
<ol>
<li> Сети позиций и переходов. Мультимножества и операции над ними. Разметки. Сети Петри.
<li> Условия срабатывания переходов. Отношение срабатывания переходов. Вычисления обыкновенных сетей Петри. Достижимые и тупиковые разметки. Граф достижимых разметок обыкновенной сети Петри.
<li> Сравнение разметок. Теорема о свойстве монотонности вычислений обыкновенных сетей Петри.
<li> Свойства ограниченности, безопасности и консервативности сетей Петри.
<li> Свойства живости и устойчивости сетей Петри.
<li> Проблемы достижимости и R-эквивалентности для сетей Петри.
<li> Моделирование многочленов обыкновенными сетями Петри. Неразрешимость проблемы R-эквивалентности для обыкновенных сетей Петри.
<li> Языки, порождаемые сетями Петри. Примеры языков, порождаемых сетями Петри. Сравнение класса языков, порождаемых обыкновенными сетями Петри, и классов языков иерархии Хомского.
<li> Ординарные сети Петри. Моделирование обыкновенных сетей Петри ординарными сетями.
<li> Автоматные сети Петри. Моделирование конечных автоматов автоматными сетями Петри.
<li> Синхронизационные сети Петри. Условия живости и консервативности для синхронизационных сетей Петри.
<li> Сети потоков работ.
<li> Ингибиторные сети Петри. Моделирование счетчиковых машин Минского ингибиторными сетями Петри.
<li> Раскрашенные сети Петри.
</ol>

== Схемы программ ==
<ol start="15">
<li> Проблема эквивалентности программ и трудности ее решения. Моделирование программ схемами программ.
<li> Стандартные схемы программ: синтаксис и семантика. Вычисления стандартных схем программ.
<li> Задачи анализа поведения стандартных схем программ - проблемы пустоты, эквивалентности, свободы схем программ.
<li> Представление стандартных схем программ при помощи систем переходов и алгебры подстановок.
<li> Эрбрановские интерпретации для стандартных схем программ. Эквивалентность стандартных схем программ на эрбрановских интерпретациях.
<li> Неразрешимость проблем анализа поведения стандартных схем программ.
<li> Схемы программ Ляпунова-Янова.
<li> Взаимосвязь схем программ Ляпунова-Янова и конечных автоматов. Разрешимость проблемы эквивалентности для схем Ляпунова-Янова.
</ol>

== Алгебра процессов ==
<ol start="23">
<li> Базовая алгебра процессов.
<li> Алгебра процессов с параллелизмом.
<li> Алгебра взаимодействующих процессов.
<li> Процессные графы.
<li> Бисимуляция процессов.
<li> Консервативное расширение алгебры процессов.
<li> Рекурсия в алгебре процессов.
</ol>

= Литература =

<ol>
<li> Котов В.Е. Сети Петри - М.: Мир, 1984.
<li> Питерсон Дж. Теория сетей Петри и моделирование систем. - М.: Мир, 1984.
<li> Ломазова И.А. Вложенные сети Петри: моделирование м анализ распределенных систем с объектной структурой - М.: Научный мир, 2004.
<li> Reisig W. Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. - Springer, 2013.
<li> Котов В.Е., Сабельфельд В.К. Теория схем программ - М.: Мир, 1983.
<li> Fokkink W. Introduction to process algebra. Springer Berlin, Heidelberg, 2000
</ol>

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

2023-08-29T10:46:20Z

#перенаправление [[Математические модели последовательных вычислений]]

Математическая логика (318, 319/2, 241, 242)

2023-08-29T10:45:04Z

Root:

[[Категория:Лекционные курсы кафедры МК]]

Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].

Актуальность информации: весенний семестр 2022/2023 учебного года.

= Слайды лекций =

[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.

[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.

[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.

[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).

[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.

[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).

[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?

[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.

[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).

[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.

[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.

[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.

[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.

[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.

[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.

[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).

[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).

[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.

[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.

[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.

[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.

[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.

[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).

[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.

[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.

[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.

[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.

[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.

[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.

[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.

[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).

[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.

[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).

[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.

[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.

[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.

[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.

[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.

[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.

[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.

[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.

[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.

[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.

[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.

[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.

[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.

[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.

[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.

[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.

[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.

[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.

= Семинары =

''Материалы семинаров будут обновляться по мере проведения занятий''

Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]

Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]

[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]

= Контрольные работы =

Контрольные работы проводятся письменно, длительность каждой - 90 минут.

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

Оценка решений типовых задач:
* Максимальная оценка - 4 балла.
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.
* Если в решении обнаружены правильные элементы, но в малом количестве, то задача оценивается в 1 балл.

Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
Правильно решённый теоретический вопрос оценивается в 1 балл.

'''Первая контрольная работа''' будет содержать 3 типовые задачи (по темам 1-3) и 9 теоретических вопросов (по прочитанным лекциям).

'''Вторая контрольная работа''' будет содержать все типовые задачи и 5 теоретических вопросов (по темам, не попавшим в первую контрольную работу).

'''Остальные контрольные работы''' будут содержать все типовые задачи и 14 теоретических вопросов (по всем темам лекций).

= Зачёт =

На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
При проставлении зачёта учитывается 6 технических оценок:
* Четыре оценки за типовые задачи, по одной за каждую задачу.
* Оценка за знание теории. Максимум - 14 баллов.
* Оценка за решение премиальных задач.

Для получения зачёта требуется достичь следующих результатов:
# Набрать хотя бы 11 баллов за типовые задачи.
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).

Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].

Для решения каждой типовой задачи будет предложено несколько попыток.
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.

При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных
* суммарно за первые две контрольные работы и
* за каждую из следующих контрольных работ.

= Экзамен =

Формат проведения и длительность экзамена: письменно, 120 минут.

Экзаменационная работа оценивается по шкале от 0 до 30 технических баллов.
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].
Согласно набранной сумме технических баллов выставляется оценка:
* хотя бы 24: '''отлично''';
* хотя бы 18, но менее 24: '''хорошо''';
* хотя бы 12, но менее 18: '''удовлетворительно''';
* менее 12: '''неудовлетворительно'''.

Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
* Каждая из задач 1-4 оценивается в 3 балла. Темы задач:
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
*# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
*# Проверить общезначимость формулы логики предикатов методом резолюций.
*# Доказать формулу в натуральном исчислении предикатов.
* Каждая из задач 5-7 оценивается в 2 балла и состоит из двух частей:
*# Сформулировать утверждение, определение и т.п.
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
* Каждая из задач 8-11 оценивается в 3 балла и устроена так:
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
** Невыбранные ответы обосновывать не нужно.

== Контрольная работа ==

На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].
Максимальная техническая оценка за эту работу - 21 балл.
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:
* набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;
* набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;
* набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;
* набрано хотя бы 10, но менее 13 баллов: бонус <span style="background:#DDFFDD">+0 баллов</span>;
* набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;
* набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;
* набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;
* контрольная работа пропущена по неуважительной причине: штраф <span style="background:#FFDDDD">-3 балла</span>;
* контрольная работа пропущена по уважительной причине: бонус <span style="background:#DDFFDD">+0 баллов</span>.

= Премиальные задачи =

Общие условия сдачи решений премиальных задач:
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для их решения может потребоваться дополнительное устное обсуждение.
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.

'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой.
Например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 319/2, а также ...''".

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

= Программа курса =

''Программа будет обновляться согласно фактически прочитанному материалу''

== Классические логики ==
<ol>
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
<li> Машины Тьюринга. Теорема Чёрча.
<li> Равносильные формулы. Теорема о равносильной замене.
</ol>

== Метод резолюций в логике предикатов ==
<ol start="10">
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
<li> Метод резолюций: общая схема, применение.
</ol>

== Логические исчисления ==
<ol start="19">
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.
<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).
</ol>

== Аксиоматические теории ==
<ol start="23">
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).
<li> Арифметика Пресбургера, её разрешимость и выразительность.
</ol>

== Неклассические прикладные логики ==
<ol start="28">
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
<li> Интуиционистская логика.
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.
</ol>

= Рекомендованная литература =

== Основная литература ==
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.

== Дополнительная литература ==

# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.

Математическая логика (318, 319/2, 241, 242)

2023-08-29T10:44:41Z

Root: Root переименовал страницу Математическая логика и логическое программирование (группа 318) в Математическая логика (318, 319/2, 241, 242): Актуа…

Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].

Актуальность информации: весенний семестр 2022/2023 учебного года.

= Слайды лекций =

[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.

[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.

[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.

[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).

[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.

[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).

[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?

[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.

[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).

[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.

[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.

[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.

[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.

[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.

[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.

[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).

[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).

[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.

[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.

[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.

[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.

[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.

[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).

[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.

[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.

[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.

[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.

[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.

[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.

[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.

[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).

[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.

[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).

[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.

[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.

[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.

[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.

[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.

[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.

[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.

[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.

[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.

[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.

[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.

[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.

[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.

[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.

[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.

[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.

[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.

[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.

= Семинары =

''Материалы семинаров будут обновляться по мере проведения занятий''

Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]

Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]

[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]

= Контрольные работы =

Контрольные работы проводятся письменно, длительность каждой - 90 минут.

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

Оценка решений типовых задач:
* Максимальная оценка - 4 балла.
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.
* Если в решении обнаружены правильные элементы, но в малом количестве, то задача оценивается в 1 балл.

Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
Правильно решённый теоретический вопрос оценивается в 1 балл.

'''Первая контрольная работа''' будет содержать 3 типовые задачи (по темам 1-3) и 9 теоретических вопросов (по прочитанным лекциям).

'''Вторая контрольная работа''' будет содержать все типовые задачи и 5 теоретических вопросов (по темам, не попавшим в первую контрольную работу).

'''Остальные контрольные работы''' будут содержать все типовые задачи и 14 теоретических вопросов (по всем темам лекций).

= Зачёт =

На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
При проставлении зачёта учитывается 6 технических оценок:
* Четыре оценки за типовые задачи, по одной за каждую задачу.
* Оценка за знание теории. Максимум - 14 баллов.
* Оценка за решение премиальных задач.

Для получения зачёта требуется достичь следующих результатов:
# Набрать хотя бы 11 баллов за типовые задачи.
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).

Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].

Для решения каждой типовой задачи будет предложено несколько попыток.
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.

При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных
* суммарно за первые две контрольные работы и
* за каждую из следующих контрольных работ.

= Экзамен =

Формат проведения и длительность экзамена: письменно, 120 минут.

Экзаменационная работа оценивается по шкале от 0 до 30 технических баллов.
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].
Согласно набранной сумме технических баллов выставляется оценка:
* хотя бы 24: '''отлично''';
* хотя бы 18, но менее 24: '''хорошо''';
* хотя бы 12, но менее 18: '''удовлетворительно''';
* менее 12: '''неудовлетворительно'''.

Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
* Каждая из задач 1-4 оценивается в 3 балла. Темы задач:
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
*# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
*# Проверить общезначимость формулы логики предикатов методом резолюций.
*# Доказать формулу в натуральном исчислении предикатов.
* Каждая из задач 5-7 оценивается в 2 балла и состоит из двух частей:
*# Сформулировать утверждение, определение и т.п.
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
* Каждая из задач 8-11 оценивается в 3 балла и устроена так:
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
** Невыбранные ответы обосновывать не нужно.

== Контрольная работа ==

На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].
Максимальная техническая оценка за эту работу - 21 балл.
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:
* набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;
* набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;
* набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;
* набрано хотя бы 10, но менее 13 баллов: бонус <span style="background:#DDFFDD">+0 баллов</span>;
* набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;
* набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;
* набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;
* контрольная работа пропущена по неуважительной причине: штраф <span style="background:#FFDDDD">-3 балла</span>;
* контрольная работа пропущена по уважительной причине: бонус <span style="background:#DDFFDD">+0 баллов</span>.

= Премиальные задачи =

Общие условия сдачи решений премиальных задач:
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для их решения может потребоваться дополнительное устное обсуждение.
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.

'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой.
Например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 319/2, а также ...''".

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

= Программа курса =

''Программа будет обновляться согласно фактически прочитанному материалу''

== Классические логики ==
<ol>
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
<li> Машины Тьюринга. Теорема Чёрча.
<li> Равносильные формулы. Теорема о равносильной замене.
</ol>

== Метод резолюций в логике предикатов ==
<ol start="10">
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
<li> Метод резолюций: общая схема, применение.
</ol>

== Логические исчисления ==
<ol start="19">
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.
<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).
</ol>

== Аксиоматические теории ==
<ol start="23">
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).
<li> Арифметика Пресбургера, её разрешимость и выразительность.
</ol>

== Неклассические прикладные логики ==
<ol start="28">
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
<li> Интуиционистская логика.
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.
</ol>

= Рекомендованная литература =

== Основная литература ==
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.

== Дополнительная литература ==

# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.

Математическая логика и логическое программирование (группа 318)

2023-08-29T10:44:41Z

#перенаправление [[Математическая логика (318, 319/2, 241, 242)]]

Языки описания схем

2023-08-29T10:41:23Z

Root:

[[Категория:Лекционные курсы кафедры МК]]
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]

''Актуальность информации: осенний семестр 2022/2023 учебного года.''

Обязательный курс для студентов группы 518мк_дус. Курс проводит [[Подымов Владислав Васильевич|Подымов В.В.]]

= Материалы занятий =

'''[[Media: Hdl_lecture_01.pdf|Блок 1.]]''' Организационные вопросы.

'''[[Media: Hdl_lecture_02.pdf|Блок 2.]]''' Вспоминаем дискретную математику: булевы функции, булевы формулы, схемы из функциональных элементов.

'''[[Media: Hdl_lecture_03.pdf|Блок 3.]]''' Как устроена цифровая аппаратура. Немного физики: как схемы из функциональных элементов связаны с реальным миром.

'''[[Media: Hdl_lecture_04.pdf|Блок 4.]]''' Логические вентили. Комбинационные схемы.

'''[[Media: Hdl_lecture_05.pdf|Блок 5.]]''' Вспоминаем дискретную математику: схемы из функциональных элементов с задержкой.

'''[[Media: Hdl_lecture_06.pdf|Блок 6.]]''' Комбинационные схемы с обратной связью. Основные триггеры.

'''[[Media: Hdl_lecture_07.pdf|Блок 7.]]''' Ещё несколько слов о сигналах: активный уровень, передний фронт, задний фронт, такт.

'''[[Media: Hdl_lecture_08.pdf|Блок 8.]]''' Ещё несколько слов о триггерах: синхронные триггеры, асинхронные триггеры, типичные входы триггеров.

'''[[Media: Hdl_lecture_09.pdf|Блок 9.]]''' Последовательные схемы.

'''[[Media: Hdl_lecture_10.pdf|Блок 10.]]''' Шины. Регистры. Уровень регистровых передач (RTL).

'''[[Media: Hdl_practice_01.pdf|Практический блок 1.]]''' Разработка комбинационных и последовательных схем.

'''[[Media: Hdl_lecture_11.pdf|Блок 11.]]''' Verilog: от логических значений до комбинационных схем.

'''[[Media: Hdl_lecture_12.pdf|Блок 12.]]''' Verilog: основы программной симуляции.

'''[[Media: Hdl_practice_02.pdf|Практический блок 2.]]''' Verilog и непрерывное присваивание.

'''[[Media: Hdl_lecture_13.pdf|Блок 13.]]''' Verilog: синтезируемость кода

'''[[Media: Hdl_lecture_14.pdf|Блок 14.]]''' Verilog: ещё пара слов о процедурных командах.

'''[[Media: Hdl_lecture_15.pdf|Блок 15.]]''' Verilog: аппаратная семантика постоянной процедуры.

'''[[Media: Hdl_practice_03.pdf|Практический блок 3.]]''' Verilog и процедуры.

'''[[Media: Hdl_lecture_16.pdf|Блок 16.]]''' Вспоминаем дискретную математику: автоматы.

'''[[Media: Hdl_lecture_17.pdf|Блок 17.]]''' Автоматы и синхронные схемы.

'''[[Media: Hdl_lecture_18.pdf|Блок 18.]]''' Пара слов о символьных автоматах.

'''[[Media: Hdl_practice_04.pdf|Практический блок 4.]]''' Автоматы.

'''[[Media: Hdl_lecture_19.pdf|Блок 19.]]''' Verilog: немного синтаксического сахара.

'''[[Media: Hdl_practice_05.pdf|Практический блок 5.]]''' Verilog и продвинутый синтаксис: параметры, массивы, генерация.

'''[[Media: Hdl_lecture_20.pdf|Блок 20.]]''' Verilog: как реализовать автомат.

'''[[Media: Hdl_lecture_21.pdf|Блок 21.]]''' "Грамотная" разработка схем. Данные и управление. Операционный и управляющий автоматы.

'''[[Media: Hdl_lecture_22.pdf|Блок 22.]]''' Как спроектировать операционный автомат.

'''[[Media: Hdl_lecture_23.pdf|Блок 23.]]''' Как дополнить операционный автомат управляющим.

'''[[Media: Hdl_lecture_24.pdf|Блок 24.]]''' Как уменьшить автомат. Автоматы с таймерами.

'''[[Media: Hdl_practice_06.pdf|Практический блок 6.]]''' Операционный и управляющий автоматы в Verilog.

'''[[Media: Hdl_lecture_aux_01.pdf|Кое-что ещё 1.]]''' Протоколы передачи данных. Общее описание протокола UART.

'''[[Media: Hdl_lecture_aux_02.pdf|Кое-что ещё 2.]]''' Схемная реализация протокола UART.

'''[[Media: Hdl_lecture_aux_03.pdf|Кое-что ещё 3.]]''' Классификация протоколов передачи данных.

'''[[Media: Hdl_lecture_aux_04.pdf|Кое-что ещё 4.]]''' Протокол SPI для двух устройств.

'''[[Media: Hdl_lecture_aux_05.pdf|Кое-что ещё 5.]]''' Протокол SPI для произвольного числа устройств. Состояние высокого импеданса.

= Условия получения зачёта =

(Cм. слайды "Блок 1")
Для получения зачёта достаточно '''в срок''' сдать решения четырёх заданий, которые будут выдаваться по мере проведения занятий.
Если хотя бы одно решение не сдано в срок, то для получения зачёта потребуется выполнить особое ''штрафное задание''.

= Литература =
== Основная ==
* Harris, Harris. Digital Design and Computer Architecture, 2nd Edition. Elseveir. 2013.
** Перевод: "Харрис, Харрис. Цифровая схемотехника и архитектура компьютера. ДМК Пресс. 2018."
** В сети в открытом доступе лежат и другие версии перевода (не выпущенные официально в печать).
* Thomas, Moorby. The Verilog Hardware Description Language, 5th Edition. Springer. 2008.

== Дополнительная ==
* Hennesy, Patterson. Computer Organization and Design: The Hardware/Software Interface, 5th Edition. Morgan Kaufmann. 2013.
* Palnitkar. Verilog HDL, 2nd Edition. 2003.
* Vahid. Digital Design with RTL Design, VHDL, and Verilog, 2nd Edition. Wiley. 2010.

Языки описания схем

2023-08-29T10:41:03Z

Root: Root переименовал страницу Языки описания цифровых схем в Языки описания схем: Было неточное название

''Актуальность информации: осенний семестр 2022/2023 учебного года.''

Обязательный курс для студентов группы 518мк_дус. Курс проводит [[Подымов Владислав Васильевич|Подымов В.В.]]

= Материалы занятий =

'''[[Media: Hdl_lecture_01.pdf|Блок 1.]]''' Организационные вопросы.

'''[[Media: Hdl_lecture_02.pdf|Блок 2.]]''' Вспоминаем дискретную математику: булевы функции, булевы формулы, схемы из функциональных элементов.

'''[[Media: Hdl_lecture_03.pdf|Блок 3.]]''' Как устроена цифровая аппаратура. Немного физики: как схемы из функциональных элементов связаны с реальным миром.

'''[[Media: Hdl_lecture_04.pdf|Блок 4.]]''' Логические вентили. Комбинационные схемы.

'''[[Media: Hdl_lecture_05.pdf|Блок 5.]]''' Вспоминаем дискретную математику: схемы из функциональных элементов с задержкой.

'''[[Media: Hdl_lecture_06.pdf|Блок 6.]]''' Комбинационные схемы с обратной связью. Основные триггеры.

'''[[Media: Hdl_lecture_07.pdf|Блок 7.]]''' Ещё несколько слов о сигналах: активный уровень, передний фронт, задний фронт, такт.

'''[[Media: Hdl_lecture_08.pdf|Блок 8.]]''' Ещё несколько слов о триггерах: синхронные триггеры, асинхронные триггеры, типичные входы триггеров.

'''[[Media: Hdl_lecture_09.pdf|Блок 9.]]''' Последовательные схемы.

'''[[Media: Hdl_lecture_10.pdf|Блок 10.]]''' Шины. Регистры. Уровень регистровых передач (RTL).

'''[[Media: Hdl_practice_01.pdf|Практический блок 1.]]''' Разработка комбинационных и последовательных схем.

'''[[Media: Hdl_lecture_11.pdf|Блок 11.]]''' Verilog: от логических значений до комбинационных схем.

'''[[Media: Hdl_lecture_12.pdf|Блок 12.]]''' Verilog: основы программной симуляции.

'''[[Media: Hdl_practice_02.pdf|Практический блок 2.]]''' Verilog и непрерывное присваивание.

'''[[Media: Hdl_lecture_13.pdf|Блок 13.]]''' Verilog: синтезируемость кода

'''[[Media: Hdl_lecture_14.pdf|Блок 14.]]''' Verilog: ещё пара слов о процедурных командах.

'''[[Media: Hdl_lecture_15.pdf|Блок 15.]]''' Verilog: аппаратная семантика постоянной процедуры.

'''[[Media: Hdl_practice_03.pdf|Практический блок 3.]]''' Verilog и процедуры.

'''[[Media: Hdl_lecture_16.pdf|Блок 16.]]''' Вспоминаем дискретную математику: автоматы.

'''[[Media: Hdl_lecture_17.pdf|Блок 17.]]''' Автоматы и синхронные схемы.

'''[[Media: Hdl_lecture_18.pdf|Блок 18.]]''' Пара слов о символьных автоматах.

'''[[Media: Hdl_practice_04.pdf|Практический блок 4.]]''' Автоматы.

'''[[Media: Hdl_lecture_19.pdf|Блок 19.]]''' Verilog: немного синтаксического сахара.

'''[[Media: Hdl_practice_05.pdf|Практический блок 5.]]''' Verilog и продвинутый синтаксис: параметры, массивы, генерация.

'''[[Media: Hdl_lecture_20.pdf|Блок 20.]]''' Verilog: как реализовать автомат.

'''[[Media: Hdl_lecture_21.pdf|Блок 21.]]''' "Грамотная" разработка схем. Данные и управление. Операционный и управляющий автоматы.

'''[[Media: Hdl_lecture_22.pdf|Блок 22.]]''' Как спроектировать операционный автомат.

'''[[Media: Hdl_lecture_23.pdf|Блок 23.]]''' Как дополнить операционный автомат управляющим.

'''[[Media: Hdl_lecture_24.pdf|Блок 24.]]''' Как уменьшить автомат. Автоматы с таймерами.

'''[[Media: Hdl_practice_06.pdf|Практический блок 6.]]''' Операционный и управляющий автоматы в Verilog.

'''[[Media: Hdl_lecture_aux_01.pdf|Кое-что ещё 1.]]''' Протоколы передачи данных. Общее описание протокола UART.

'''[[Media: Hdl_lecture_aux_02.pdf|Кое-что ещё 2.]]''' Схемная реализация протокола UART.

'''[[Media: Hdl_lecture_aux_03.pdf|Кое-что ещё 3.]]''' Классификация протоколов передачи данных.

'''[[Media: Hdl_lecture_aux_04.pdf|Кое-что ещё 4.]]''' Протокол SPI для двух устройств.

'''[[Media: Hdl_lecture_aux_05.pdf|Кое-что ещё 5.]]''' Протокол SPI для произвольного числа устройств. Состояние высокого импеданса.

= Условия получения зачёта =

(Cм. слайды "Блок 1")
Для получения зачёта достаточно '''в срок''' сдать решения четырёх заданий, которые будут выдаваться по мере проведения занятий.
Если хотя бы одно решение не сдано в срок, то для получения зачёта потребуется выполнить особое ''штрафное задание''.

= Литература =
== Основная ==
* Harris, Harris. Digital Design and Computer Architecture, 2nd Edition. Elseveir. 2013.
** Перевод: "Харрис, Харрис. Цифровая схемотехника и архитектура компьютера. ДМК Пресс. 2018."
** В сети в открытом доступе лежат и другие версии перевода (не выпущенные официально в печать).
* Thomas, Moorby. The Verilog Hardware Description Language, 5th Edition. Springer. 2008.

== Дополнительная ==
* Hennesy, Patterson. Computer Organization and Design: The Hardware/Software Interface, 5th Edition. Morgan Kaufmann. 2013.
* Palnitkar. Verilog HDL, 2nd Edition. 2003.
* Vahid. Digital Design with RTL Design, VHDL, and Verilog, 2nd Edition. Wiley. 2010.

Языки описания цифровых схем

2023-08-29T10:41:03Z

Root: Root переименовал страницу Языки описания цифровых схем в Языки описания схем: Было неточное название

#перенаправление [[Языки описания схем]]

Проектирование больших систем на С++

2023-08-23T14:50:53Z

Root:

Занятия в осеннем семестре 2022 г. завершены.

Курс по магистерской программе Дискретные управляющие системы и их приложения. Занятия проводит [[Участник:KonovodovV|Коноводов В.А.]]

В курсе рассматриваются темы, востребованные в промышленном программировании на языке C++. Разбираются вопросы, связанные с обобщенным программированием, интеллектуальными указателями, исключениями, паттернами проектирования, тестированием и отладкой кода, и др. Отдельно разбираются возможности современного языка С++, введенные в стандартах C++11/14/17: вывод типов, семантика перемещения, rvalue-ссылки, поддержка многопоточности, лямбда-выражения и др.

В задачи курса входят актуализация студентами знаний языка С++ и ознакомление с современными принципами проектирования больших систем с использованием языка C++.
На занятиях предполагается разбор примеров использования конструкций языка и применения рассматриваемых методов проектирования, а также проведение промежуточных небольших тестов-контрольных.

[[Media: Pbscpp_content_2022.pdf|Программа курса 2022(pdf)]]

== Занятия в 2022 г ==
* Занятия завершены.
* Таблица результатов [https://docs.google.com/spreadsheets/d/1Exq4vDEQ2eg82WZLEmjTKfE-C334_uOtnzraGMdnz50 здесь]

== Экзамен ==
Экзамен по курсу письменный. Максимальная сумма баллов за экзаменационную работу – 50. Баллы, полученные за выполнение необязательных домашних задач и тестов на занятиях, суммируются с баллами, полученными за экзамен.

* Оценка '''отлично''': не менее 40 баллов
* Оценка '''хорошо''': не менее 30 и не более 39 баллов
* Оценка '''удовлетворительно''': не менее 20 и не более 29 баллов

Примеры экзаменационных задач: [[Media: cpp_exam_demo.pdf|pdf]].

== Содержание курса ==
'''Занятие 1.''' Вводный тест. Некоторые особенности C++11, вывод типа.

'''Занятие 2.''' Модификаторы функций, псевдонимы, scoped enums. Constexpr-выражения и объекты. Шаблоны с переменным числом аргументов.
* [https://disk.yandex.ru/i/LLhLfKUrtxM5Ug Лекции 1-2]
* [https://disk.yandex.ru/i/0zz99oSXBbX6Qg Задача] (больше не принимается)

'''Занятие 3.''' Лямбда-выражения. Структурное связывание. Неупорядоченные контейнеры. Вызовы функций.
* [https://disk.yandex.ru/i/ntdIW0Go_MPKog Лекция 3]

'''Занятие 4.''' Move-семантика, типы ссылок. Проблема перегрузки универсальных ссылок.
* [https://disk.yandex.ru/i/4LGYLn2L_2bupA Лекция 4]
* [https://disk.yandex.ru/i/jisLZBBHGoln0g Запись]
* [https://disk.yandex.ru/i/VYfxjjh17NtYRg Задачи] (больше не принимается)

'''Занятие 5.''' Особенности перемещающих операций в классах. Умные указатели.
* [https://disk.yandex.ru/d/3kTuofEnSVWIsA Лекция 5]
* [https://disk.yandex.ru/i/S6jW75TBRi3qEg Запись]
* [https://disk.yandex.ru/i/dI1xkV7mZrpmkQ Задача] (больше не принимается)

'''Занятие 6.''' Умные указатели и владение памятью. Идиома CRTP.
* [https://disk.yandex.ru/i/uPzr89AF4zrv-Q Лекция 6]
* [https://disk.yandex.ru/i/RyTb7iq0unfprA Запись]
* [https://disk.yandex.ru/i/ePt7dk53Iem4fQ Задача] и [https://github.com/konovodov/-cmc_msu_cpp_course2021/tree/main код] к ней (больше не принимается)

'''Занятие 7.''' Идиома PImpl. Паттерны проектирования Bridge, Command, Strategy, Singleton.
* [https://disk.yandex.ru/i/uH6561AFNRS4aw Лекция 7]
* [https://disk.yandex.ru/i/Ef_-x_nandwIgg Запись]

'''Занятие 8.''' Создание объектов с помощью фабрик. Паттерны проектирования Decorator и Visitor.
* [https://disk.yandex.ru/i/jMw0tBnMgH9vbQ Лекция 8]
* [https://disk.yandex.ru/i/5upciy1jo7s67A Запись]

'''Занятие 9.''' Идиома TypeErasure. Решение проблем перегрузки универсальных ссылок. Диспетчеризация дескрипторов. Правило SFINAE.
* [https://disk.yandex.ru/i/zV2fe1AVusaMDg Лекция 9]
* [https://disk.yandex.ru/i/TN3QQUHCIOBt6w Запись]
* [https://disk.yandex.ru/i/O0_xPykHi9gPbQ Задачи] (больше не принимаются)

'''Занятие 10.''' Обработка исключений. Гарантии безопасности исключений. Неопределенное поведение.
* [https://disk.yandex.ru/d/EOLsv_3KAfUcSg Лекция 10]
* [https://disk.yandex.ru/i/6jITF-YaW0n6_Q Запись]

'''Занятие 11.''' Тестирование кода, unit-тестирование, устранение зависимостей. Google C++ Testing Framework.
* [https://disk.yandex.ru/i/1r0rTlv7tm-GCQ Лекция 11]
* [https://disk.yandex.ru/i/kpkxZnzU8GX86Q Запись]
* [https://github.com/konovodov/-cmc_msu_cpp_course2021/tree/main/testing пример] кода с занятия
* [https://disk.yandex.ru/i/2wiQon6oTY_ZKA Задачи] (больше не принимаются)

'''Занятие 12.''' Отладка и дебаг кода. Оптимизация программ на C++. Строки.
* [https://disk.yandex.ru/i/Nvu2219cQk7suQ Лекция 12]
* [https://disk.yandex.ru/i/xHhpvZda4o7x-g Запись]
* [https://disk.yandex.ru/i/wIkIR4l1KoMlLg Задача] (больше не принимается)

'''Занятие 13.''' Оптимизация алгоритмов, функций, памяти. Плотная упаковка полей. Бинарная сериализация данных. Protobuf.
* [https://disk.yandex.ru/i/3aPdb6gO7767ig Лекция 13]
* [https://disk.yandex.ru/i/zinAW8OvEoYcsA Запись]
* [https://disk.yandex.ru/i/vE7LwXekadSUcw Задача] и [https://disk.yandex.ru/d/_9udeF-WPVN9qA пример] входного файла к ней. (Больше не принимается). Комментарии по проверке находятся в отдельном листе таблицы результатов.

== Литература ==
===Основная===
* С. Мейерс, Эффективный и современный С++: 42 рекомендации по использованию C++11 и C++14, изд. Вильямс, М.: 2017 г.
* Ф. Пикус, Идиомы и паттерны проектирования в современном C++. ДМК Пресс, 2019 г.
* CppCoreGuidelines (ред. Б. Страуструп, Г. Саттер) https://isocpp.github.io/CppCoreGuidelines/CppCoreGuidelines
* Курт Гантерот: Оптимизация программ на C++. Проверенные методы повышения производительности. М.:Диалектика, 2017 г.

===Дополнительная===
* Klaus Iglberger. C++ Software Design: Design Principles and Patterns for High-Quality Software. O'Reilly Media; 1st edition. 2022.
* Anthony Williams. C++ Concurrency in Action: Practical Multithreading.
* А. Александреску, Современное проектирование на C++, изд. Вильямс, М.: 2017 г.
* Э.Гамма, Р.Хелм, Р.Джонсон, Дж. Влиссидес, Приемы объектно-ориентированного проектирования.
* Г. Саттер, А. Александреску, Стандарты программирования на С++. 101 правило и рекомендация.
* Б. Страуструп, Язык программирования С++, 4-е издание.
* Б. Страуструп, Программирование. Принципы и практика использования C++.
* Вандевурд Д., Джосаттис Н. Шаблоны C++. Справочник разработчика.
* Курс [https://academy.yandex.ru/handbook/cpp Основы C++] от Академии Яндекса.
* [http://google.github.io/googletest/ Документация] по Google Test.
* [https://developers.google.com/protocol-buffers/docs/overview?hl=en Документация] protobuf.

[[Категория:Лекционные курсы кафедры МК]]
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]

Проектирование больших систем С++

2023-08-23T14:49:28Z

Root: Root переименовал страницу Проектирование больших систем С++ в Проектирование больших систем на С++: опечатка

#перенаправление [[Проектирование больших систем на С++]]

Проектирование больших систем на С++

2023-08-23T14:49:27Z

{{DISPLAYTITLE:Проектирование больших систем на С++}}
Занятия в осеннем семестре 2022 г. завершены.

Курс по магистерской программе Дискретные управляющие системы и их приложения. Занятия проводит [[Участник:KonovodovV|Коноводов В.А.]]

В курсе рассматриваются темы, востребованные в промышленном программировании на языке C++. Разбираются вопросы, связанные с обобщенным программированием, интеллектуальными указателями, исключениями, паттернами проектирования, тестированием и отладкой кода, и др. Отдельно разбираются возможности современного языка С++, введенные в стандартах C++11/14/17: вывод типов, семантика перемещения, rvalue-ссылки, поддержка многопоточности, лямбда-выражения и др.

В задачи курса входят актуализация студентами знаний языка С++ и ознакомление с современными принципами проектирования больших систем с использованием языка C++.
На занятиях предполагается разбор примеров использования конструкций языка и применения рассматриваемых методов проектирования, а также проведение промежуточных небольших тестов-контрольных.

[[Media: Pbscpp_content_2022.pdf|Программа курса 2022(pdf)]]

== Занятия в 2022 г ==
* Занятия завершены.
* Таблица результатов [https://docs.google.com/spreadsheets/d/1Exq4vDEQ2eg82WZLEmjTKfE-C334_uOtnzraGMdnz50 здесь]

== Экзамен ==
Экзамен по курсу письменный. Максимальная сумма баллов за экзаменационную работу – 50. Баллы, полученные за выполнение необязательных домашних задач и тестов на занятиях, суммируются с баллами, полученными за экзамен.

* Оценка '''отлично''': не менее 40 баллов
* Оценка '''хорошо''': не менее 30 и не более 39 баллов
* Оценка '''удовлетворительно''': не менее 20 и не более 29 баллов

Примеры экзаменационных задач: [[Media: cpp_exam_demo.pdf|pdf]].

== Содержание курса ==
'''Занятие 1.''' Вводный тест. Некоторые особенности C++11, вывод типа.

'''Занятие 2.''' Модификаторы функций, псевдонимы, scoped enums. Constexpr-выражения и объекты. Шаблоны с переменным числом аргументов.
* [https://disk.yandex.ru/i/LLhLfKUrtxM5Ug Лекции 1-2]
* [https://disk.yandex.ru/i/0zz99oSXBbX6Qg Задача] (больше не принимается)

'''Занятие 3.''' Лямбда-выражения. Структурное связывание. Неупорядоченные контейнеры. Вызовы функций.
* [https://disk.yandex.ru/i/ntdIW0Go_MPKog Лекция 3]

'''Занятие 4.''' Move-семантика, типы ссылок. Проблема перегрузки универсальных ссылок.
* [https://disk.yandex.ru/i/4LGYLn2L_2bupA Лекция 4]
* [https://disk.yandex.ru/i/jisLZBBHGoln0g Запись]
* [https://disk.yandex.ru/i/VYfxjjh17NtYRg Задачи] (больше не принимается)

'''Занятие 5.''' Особенности перемещающих операций в классах. Умные указатели.
* [https://disk.yandex.ru/d/3kTuofEnSVWIsA Лекция 5]
* [https://disk.yandex.ru/i/S6jW75TBRi3qEg Запись]
* [https://disk.yandex.ru/i/dI1xkV7mZrpmkQ Задача] (больше не принимается)

'''Занятие 6.''' Умные указатели и владение памятью. Идиома CRTP.
* [https://disk.yandex.ru/i/uPzr89AF4zrv-Q Лекция 6]
* [https://disk.yandex.ru/i/RyTb7iq0unfprA Запись]
* [https://disk.yandex.ru/i/ePt7dk53Iem4fQ Задача] и [https://github.com/konovodov/-cmc_msu_cpp_course2021/tree/main код] к ней (больше не принимается)

'''Занятие 7.''' Идиома PImpl. Паттерны проектирования Bridge, Command, Strategy, Singleton.
* [https://disk.yandex.ru/i/uH6561AFNRS4aw Лекция 7]
* [https://disk.yandex.ru/i/Ef_-x_nandwIgg Запись]

'''Занятие 8.''' Создание объектов с помощью фабрик. Паттерны проектирования Decorator и Visitor.
* [https://disk.yandex.ru/i/jMw0tBnMgH9vbQ Лекция 8]
* [https://disk.yandex.ru/i/5upciy1jo7s67A Запись]

'''Занятие 9.''' Идиома TypeErasure. Решение проблем перегрузки универсальных ссылок. Диспетчеризация дескрипторов. Правило SFINAE.
* [https://disk.yandex.ru/i/zV2fe1AVusaMDg Лекция 9]
* [https://disk.yandex.ru/i/TN3QQUHCIOBt6w Запись]
* [https://disk.yandex.ru/i/O0_xPykHi9gPbQ Задачи] (больше не принимаются)

'''Занятие 10.''' Обработка исключений. Гарантии безопасности исключений. Неопределенное поведение.
* [https://disk.yandex.ru/d/EOLsv_3KAfUcSg Лекция 10]
* [https://disk.yandex.ru/i/6jITF-YaW0n6_Q Запись]

'''Занятие 11.''' Тестирование кода, unit-тестирование, устранение зависимостей. Google C++ Testing Framework.
* [https://disk.yandex.ru/i/1r0rTlv7tm-GCQ Лекция 11]
* [https://disk.yandex.ru/i/kpkxZnzU8GX86Q Запись]
* [https://github.com/konovodov/-cmc_msu_cpp_course2021/tree/main/testing пример] кода с занятия
* [https://disk.yandex.ru/i/2wiQon6oTY_ZKA Задачи] (больше не принимаются)

'''Занятие 12.''' Отладка и дебаг кода. Оптимизация программ на C++. Строки.
* [https://disk.yandex.ru/i/Nvu2219cQk7suQ Лекция 12]
* [https://disk.yandex.ru/i/xHhpvZda4o7x-g Запись]
* [https://disk.yandex.ru/i/wIkIR4l1KoMlLg Задача] (больше не принимается)

'''Занятие 13.''' Оптимизация алгоритмов, функций, памяти. Плотная упаковка полей. Бинарная сериализация данных. Protobuf.
* [https://disk.yandex.ru/i/3aPdb6gO7767ig Лекция 13]
* [https://disk.yandex.ru/i/zinAW8OvEoYcsA Запись]
* [https://disk.yandex.ru/i/vE7LwXekadSUcw Задача] и [https://disk.yandex.ru/d/_9udeF-WPVN9qA пример] входного файла к ней. (Больше не принимается). Комментарии по проверке находятся в отдельном листе таблицы результатов.

== Литература ==
===Основная===
* С. Мейерс, Эффективный и современный С++: 42 рекомендации по использованию C++11 и C++14, изд. Вильямс, М.: 2017 г.
* Ф. Пикус, Идиомы и паттерны проектирования в современном C++. ДМК Пресс, 2019 г.
* CppCoreGuidelines (ред. Б. Страуструп, Г. Саттер) https://isocpp.github.io/CppCoreGuidelines/CppCoreGuidelines
* Курт Гантерот: Оптимизация программ на C++. Проверенные методы повышения производительности. М.:Диалектика, 2017 г.

===Дополнительная===
* Klaus Iglberger. C++ Software Design: Design Principles and Patterns for High-Quality Software. O'Reilly Media; 1st edition. 2022.
* Anthony Williams. C++ Concurrency in Action: Practical Multithreading.
* А. Александреску, Современное проектирование на C++, изд. Вильямс, М.: 2017 г.
* Э.Гамма, Р.Хелм, Р.Джонсон, Дж. Влиссидес, Приемы объектно-ориентированного проектирования.
* Г. Саттер, А. Александреску, Стандарты программирования на С++. 101 правило и рекомендация.
* Б. Страуструп, Язык программирования С++, 4-е издание.
* Б. Страуструп, Программирование. Принципы и практика использования C++.
* Вандевурд Д., Джосаттис Н. Шаблоны C++. Справочник разработчика.
* Курс [https://academy.yandex.ru/handbook/cpp Основы C++] от Академии Яндекса.
* [http://google.github.io/googletest/ Документация] по Google Test.
* [https://developers.google.com/protocol-buffers/docs/overview?hl=en Документация] protobuf.

[[Категория:Лекционные курсы кафедры МК]]
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]

Участник:SapozhenkoAA

2023-07-10T09:58:58Z

Root:

{{DISPLAYTITLE:Сапоженко Александр Антонович}}

<div style="background-color: #FFAAAA; border-style: dotted">
'''Актуальность информации: 2019 год.'''

'''В настоящее время не является сотрудником кафедры.'''
</div>

[[Image:Sapozhenko.jpg|thumb|right|Сапоже́нко Александр Антонович]]'''Сапоженко Александр Антонович''' — доктор физико-математических наук, профессор.

== Биография ==

Александр Антонович Сапоженко родился в Ленинграде 4 апреля 1939 г. В 1964 г. окончил Радиотехнический факультет Московского физико-технического института, а в 1967 г. аспирантуру МФТИ. В 1967 г. защитил кандидатскую диссертацию. С 1967 по 1971 г. работал в институте Математики Сибирского отделения АН СССР. С мая 1971 г. работает на факультете Вычислительной математики и кибернетики Московского государственного университета им. М.В.Ломоносова. 1993 г. - доктор ф-м. н., с 1997 г. профессор кафедры математической кибернетики факультета ВМиК МГУ.

== [[Области научных интересов]] и полученные результаты ==

Основные научные интересы А.А. Сапоженко относятся к минимизации булевых функций, случайным графам, комбинаторике, алгебре логики. В кандидатской диссертации «Геометрические свойства функций алгебры логики», защищенной им в 1967 г., получены точные значения радиуса и диаметра графа случайной булевой функции, найдена асимптотика диаметра ее графа случайной булевой функции, найдена асимптоика диаметра ее графа интервалов, описано строение компонент этого графа. Эти исследования были затем продолжены учениками А.А.Сапоженко, а также рядом зарубежных авторов.

В области минимизации булевых функций им получены оценки длины кратчайшей дизьюнктивной нормальной формы типичной булевой функции, асимптотика максимальной длины тупиковой ДНФ и асимптотика логарифма числа тупиковых ДНФ типичных функций. Эти результаты дают качественную картину локальных экстремумов в задаче минимизации типичных функций: почти все локальные экстремумы в задаче минимизации не отличаются по сложности от тривиального решения, предоставляемого совершенной ДНФ, число локальных экстремумов чрезвычайно велики, доля глобалных экстремумов среди них ничтожна, а вместе с тем решения, близкие к глобальному экстремуму, могут быть получены с помощью достаточно простого алгоритма градиентного типа.

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

Результаты, по перечислению независимых множеств в графах нашли применение в комбинаторной теории групп и теории чисел. В частности, была получена асимптотика числа множеств, свободныз от сумм, в абелевых группах четного порядка и доказана известная гипотеза Камерона-Эрдеша о числе множеств, свободных от сумм, в начальном отрезке натурального ряда.

Сапоженко А.А. является автором более 120 научных публикаций, учебных пособий, монографий и одного изобретения. Сборник задач по дискретной математике, написанный им в соавторстве с Г.П.Гавриловым, является одним из основных учебных пособий ля студентов, изучающих этот предмет в университетах и технических ВУЗах. Он был дважды издан на русском языке (в 1977, 1992 и 2004гг. Наука) и переведен на английский (1989 МИР, 1996 Kluver), испанский (1980 МИР) и венгерский (1981 Muszaki Konyvkiado) языки. Под руководством А.А.Сапоженко было защищено девять кандидатских диссертаций.

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

* [[Основы кибернетики (2 поток)]]

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

* [[Дискретная математика и математическая кибернетика]]
* [[Дискретный анализ ]]

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

# Метрические свойства почти всех булевых функций // Сб. Дискретный анализ Новосибирск — 1967 — вып. 10 — С.91-102.
# Диссертация "Метрические свойства почти всех булевых функций" // Новосибирск, ИМ СО АН СССР — 1967 — 70с.
# О наибольшей длине тупиковых д.н.ф. у почти всех функций алгебры логики // Математические заметки — 1968 — v.4, No.6, — C.649-658.
# Порядок окрестности максимальных интервалов у почти всех булевых функций // Доклады АН СССР — 968 — т. 180, No.1, C.526-530.
# Об одном доказательстве верхней оценки сложности минимальной д.н.ф. // Тезисы докладов Всесоюзной конференции по проблемам теоретической кибернетики — Новосибирск — 1969 — С.108.
# О сложности д.н.ф., получаемых с помощью градиентного алгоритма // Сб. Дискретный анализ — Новосибирск- Вып. 21, -С.62-71.
# О существенных переменных булевых функций // Сб. Дискретный анализ — Новосибирск — Вып. 23, — С.38-58.
# Геометрическое строение почти всех функций алгебры логики // Сб. Проблемы кибернетики -М.: Наука — 1975 — С.227-261
# Дизьюнктивные нормальные формы (Метрическая теория) // Издательство МГУ — 1975 — 90с.
# Сборник задач по дискретной математике // М.: Наука — 1977 368с. (Соавтор Гаврилов Г. П.)
# Обзор некоторых результатов по задачам о покрытии // Сб. Методы дискретного анализа в решении комбинаторных задач — Новосибирск — 1977 — Вып.30, -С.46-75 (Соавторы Асратян А. С. и Кузюрин Н. Н.).
# Оценка длины и числа тупиковых д.н.ф. у почти всех не всюду определенных функций алгеьры логики // Математические заметки — 1980 — т.28, No.2, -1980 — p.279-300.
# Problemas de Mathematica Dickreta (Spanish) // MIR Publisher, Moscow — 1980 -p.316 (Соавтор Gavrilov G. P.).
# Diszkret Matematikai feladatgyujtemeny (Hangarian) // Muszaki Konyvkiado, Budapest — 1981 — p.358 (with Gavrilov G. P.).
# Об отрицательных эффектах, связанных с исключением несущественных переменных // Автоматика и вычислительная техника — Рига -"Зинатне" — 1981 — С.28-35 (Соавтор Караханян Л. М.).
# О числе двоичных кодов с расстоянием 2 // Сб. Проблемы кибернетики — М.: Наука — 1983 — С.111-140 (Соавтор Коршунов А. Д.).
# Методы логического проектирования и оценки сложности // Микроэлектроника — 1984 — т.12, вып. 1, -С.42-47 (Соавтор [[Ложкин Сергей Андреевич|Ложкин С. А.]]).
# Авторское свидетельство No 1088130 // А, НОЗК 19/04, Бюллетень No 15, от 23.04.1984 (Соавторы: [[Алексеев Валерий Борисович|Алексеев В. Б.]], Корнилов В. И., [[Ложкин Сергей Андреевич|Ложкин С. А.]], Немудров В. Г.). (Изобретение).
# Минимизация булевых функций в классе д.н.ф. // Итоги науки и техники(Boolean functions minimization in the class of disjunctive normal forms (English)) — ВИНИТИ — 1987 — т.25, С.68-116 (Соавтор Чухров И. П.). (Journal of Soviet Math. Pl. Publ. Corp. — 1989 — p.2021-2052 (with Chukhrov G. P.)
# Об одном подходе к оценке пространственой сложности // Труды математического центра им. С.Банаха, Варшава — 1988 — 184-199. (Соавторы: [[Ложкин Сергей Андреевич|Ложкин С. А.]], Рыбко А. И., Шкаликова Н. А., Хромкович Ю.)
# Lower Bounds on the Area Complexity of Boolean Functions (Engl.) // Theoretical Computer Science — 1992 — v.97 — 285-300 (with Hromkovich J., [[Ложкин Сергей Андреевич|Lozkin S. A.]], Rybko A. I., Shkalikova N. A.).
# О числе связанных подмножеств с заданной мощностью границы в двудольных графах // Методы дискретного анализа в решении комбинаторных задач — Новосибирск — 1987 — вып. 45, — С.42-70.
# Асимптотика числа монотонных функций на частично упорядоченных множествах // Доклады АН СССР — 1989 — т.305 — No 2, — С.279-283. Английский перевод: Asymptotics of the number of monotone functions on partial ordered sets // Soviet Math. Doclady — 1989 vol.39 No.2 — p.289-293.
# О числе антицепей в ранжированных частично упорядоченных множествах // Дискретная математика — М.: Наука — 1989 — т.305 — No 2, С.279-283. Англ. перевод: Discrete Mathematics and Applications — Utrecht, The Nethelands, Tokio, Japan, — v.1, No.1 — p.35-59.
# О числе антицепей в многослойных ранжированных частично упорядоченных множествах // Дискретная математика — М.: Наука — 1989 — т.1, вып.1, — С.110-128. Англ. перевод: Discrete Mathematics and Applicatoins — Utretch, The Nethelands, Tokio, Japan, — v.1,No.1 — p.149-171.
# Selected Problems in Discrete Mathematics(Engl.) // — Moscow — MIR Publishers — 1989 — 414p. (with Gavrilov G.P.)
# On the number of data-bases and closure operations (English) // Theoretical Computer Sci. — North Holland — 1991 — .377-383 (with Burosch G., Demetrovich J., Katona G., Kleitman D.).
# О поиске максимально верхнего нуля монотонных функций на ранжированных частично упорядоченных множествах // Журнал математической физики и вычислительной математики — 1991 т.31, No 12, С.1871-1884.
# Задачи и упражнения по курсу дискретной математики // М.: Наука — 1992 — 408с. (Соавтор Гаврилов Г. П.)
# Метод граничных функционалов для перечислительных изопериметрических задач // Докторская диссертация — МГУ — 1993 -240с.
# Radius and Diameter of Random Subgraphs of the n-Cube(Engl.) // Random Structures and Algoritms — 1993 v.4, No.2, -p.215-229 (with Kostochka A. V., Weber K.)..
# On the Number of Closure Operations (English) // Combinatorics P.Erdos is Eighty — vol.1 Keszthely, Hungary — 1993 — p.91-105 (Burosch G., Demetrovich J., Katona G., Kleiton D.).
# О предельных распределениях случайных величин, пораждаемых ограниченными последовательностями // Дискретный Анализ — Труды Института Математики СО РАН — Т.27 — Новосибирск — 1994 -Р. 166-176.
# О возможности построения макромоделей для RC-схем // Журнал вычислительной математики и математической физики -1995 — т.35, No 12 C.1886-1898. Англ. перевод: On Possibility of Constracting Macromodels for RC-circuits // Journal of Computational Mathematics and Mathematical Physics — 1995 -т.35 No.12 -C.1886-1898..
# Problems and Exercises in Discrete Mathematics, Kluver Academic Publishers Dordrecht // Boston/ London — 1996 -p.422 (with Gavrilov G. P.).
# О числе связанных множеств с заданной мощностью окрестности в графе // Серия 1, Новосибирск — 1997 — т.4, No 3 -с. 18-34.
# Оценка числа связанных множеств в графе и структура компонент случайных подмножеств // Доклады АН, 1999, том 365, No 4, с. 455-457
# On counting boundary functional sums // Discrete Mathematics 213 (2000), 253-260.
# On the Number of Independent Sets in Bipartite Graphs with Large Minimum Degree ([http://mathcyb.cs.msu.su/paper/sapozh/bipartit.ps PostScript]) // DIMACS Technical Report 2000-25, August 2000.
# Проблема Дедекинда и метод граничных функционалов // в кн. Математические вопросы кибернетики, Вып.6 , М. Наука, 2000г. С.161-220.
# О числе независимых множеств в расширителях ([http://mathcyb.cs.msu.su/paper/sapozh/newind.ps PostScript]) // Дискретная математика, т. 13, вып. 1, 2001, с. 56-62.
# Некоторые перечислительные задачи теории графов и теории чисел // Таврический вестник математики и информатики, No 1, 2002г., С. 58-63.
# О некоторых перечислительных задачах теории графов и теории групп // Дискретный анализ и исследование операций//Материалы конференций, Новосибирск, 24-28 июня 2002г.
# Independent Sets and Sum-Free Sets // Discrete Mathematics and Applications.
# Independent sets and sum-free sets // Sixth Internetional Conference on Discrete Mathematics and Applications, Ed. Sl.Shtrakov and K.Deneke, 31.08. — 02.09.2001, Bansko, Bulgaria, 35-42.
# О числе множеств, свободных от сумм в Абелевых группах ([http://mathcyb.cs.msu.su/paper/sapozh/engruppy.ps PostScript]) // Вестник Московского Университета. Сер 1, Математика, Механика 2002. No 4. С. 14-18.
# О числе множеств, свободных от сумм, в отрезке натуральных чисел ([http://mathcyb.cs.msu.su/paper/sapozh/om-sap_5.ps PostScript]) // Дискретная математика, том 14, вып. 3, 2002, 4-7. (соавтор Омельянов К. Г.)
# Асимптотика числа множеств, свободных от сумм, в абелевых группах четного порядка // ДАН, том 383, No 4, 2002, C. 454-457.
# The Cameron-Erdos Conjecture ([http://mathcyb.cs.msu.su/paper/sapozh/trce6.ps PostScript]) // Eurocomb`2003 — Abstracts, ITI-Series, Prague, 2003 -145 p.326-327.

Подловченко Римма Ивановна

2023-07-10T09:54:10Z

Root:

[[Категория:Сотрудники кафедры математической кибернетики (архив)]]

<div style="background-color: #FFAAAA; border-style: dotted">
'''В настоящее время не является сотрудником кафедры.'''
</div>

[[Image:Podlovchenko.jpg|thumb|right|Подловченко Римма Ивановна]]'''Подловченко Римма Ивановна''' — доктор физико-математических наук, профессор [27.02.1931-17.08.2016].

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

* Теория моделей программ
* Теоретическое программирование
* Математическая кибернетика

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

* Эквивалентные преобразования в моделях вычислений
* Избранные вопросы математической теории вычислений

Участник:NagornyAS

2023-07-10T09:52:19Z

Root:

{{DISPLAYTITLE:Нагорный Александр Степанович}}

<div style="background-color: #FFAAAA; border-style: dotted">
'''Актуальность информации: 2022 год.'''

'''В настоящее время не является сотрудником кафедры.'''
</div>

[[Image:Nagorny.jpg|thumb|right|Нагорный Александр Степанович]]'''Нагорный Александр Степанович''' - кандидат физико-математических наук, старший преподаватель кафедры МК.

e-mail: anagorny1968@gmail.com

== Биография ==
Родился 21 декабря 1968 г. в Потсдаме (ГДР). Окончил с золотой медалью среднюю школу № 8 г. Слуцка Минской обл. Белорусской ССР (1986), с отличием окончил факультет вычислительной математики и кибернетики МГУ (1991). Обучался в аспирантуре факультета ВМК (1991–1994, 1995–1996). Работал приглашенным преподавателем в университете «Huanuco» (Перу, 1994–1995). В Московском университете работает с 1996 г., младший научный сотрудник (2001), ассистент (2014), старший преподаватель кафедры математической кибернетики (2015).

А.С. Нагорный принимал участие в работе лаборатории математических проблем компьютерной безопасности факультета ВМК с момента ее основания (2001). Участвует в работе оргкомитета Всероссийской олимпиады школьников по математике (с 1998), является постоянным членом оргкомитета Олимпиады школьников по прикладной математике и информатике факультета ВМК МГУ (с 2002). Преподаватель подготовительных курсов факультета ВМК (с 2000). Преподаватель ВМШ факультета ВМК (2002–2003, 2014-2015).

== [[Области научных интересов]] ==
* Статический анализ свойств программ
* Алгоритмы на дискретных структурах
* Теория частичных булевых функций
* Теория функций многозначной логики

== Основные научные результаты ==
А.С. Нагорным получена асимптотика сложности задачи сортировки k-значного n-мерного куба, поставлена и решена задача идентификации объектов, передвигающихся по k-значному n-мерному кубу, модернизирован и реализован алгоритм статического анализа программ, устанавливающий диапазоны значений индексов массивов в символьном виде.

В теории частичных булевых функций А.С. Нагорным построена решетка всех замкнутых классов частичных булевых функций, содержащих пересечение T_0 и T_1.

В теории функций k-значной логики получен ряд свойств теоретико-множественных операций над предполными классами в P_k, справедливых для всех значений k.
Полностью построена решетка основных замкнутых классов в P_3. Найдена конечная неприводимая полная система аксиом в P_3.
Также Нагорным А.С. получен ряд свойств предполных классов в 4-значной и 5-значной логике.

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

* [[Вероятностные методы в комбинаторике]]

== Семинары ==
* Дискретная математика
* Дополнительный главы дискретной математики
* Основы кибернетики
* Пакеты прикладных программ
* Элементы теории дискретных управляющих систем (318 группа)

== Спецкурсы ==

== Спецсеминары ==
* [[Некоторые вопросы теории управляющих систем]]

== Студенты и аспиранты ==

== Избранные публикации ==
# Сложность сортировки n-й декартовой степени частично упорядоченного множества // Проблемы теоретической кибернетики. Тезисы докладов XI Международной конференции (Ульяновск, 10–14 июня 1996 г.) — М.: изд. центр РГГУ, 1996, с. 148–150;
# О сложности задачи идентификации объектов, передвигающихся по k-значному n-мерному кубу // Материалы XIII международной школы-семинара «Синтез и сложность управляющих систем» (Пенза, 14-20 октября 2002 г.) — М.: изд-во Центра прикладных исследований при механико-математическом ф-те МГУ, 2002, с. 172–176;
# Сложность сортировки k-значного n-мерного куба // Труды V международной конференции «Дискретные модели в теории управляющих систем» (Ратмино, 26–29 мая 2003 г.) — М.: ф-т ВМК МГУ, 2003, с. 54–55.
# Задача идентификации объектов на k-значном n-мерном кубе // Дискретная математика и ее приложения. М.: Изд-во механико-математического факультета МГУ, 2004. С.342-344.
# О сложности задачи слепой идентификации объектов на произвольном полном конечном подграфе графа Zn // Труды VI Международной конференции «Дискретные модели в теории управляющих систем». М.: Изд. Отдел ф-та ВМК МГУ, 2004. С.190-193.
# О сложности задачи слепой идентификации // Проблемы теоретической кибернетики. Тезисы докладов XIV Международной конференции. М.: Изд-во механико-математического факультета МГУ, 2005. С.105-106.
# О структуре замкнутых классов, содержащих T01, в частичной булевой алгебре // Труды VIII Международной конференции «Дискретные модели в теории управляющих систем» (Москва, 6-9 апреля 2009 г.). М.: Изд. МАКС Пресс, 2009. С.226-227.
# О мощности базисов трехзначной логики // Научная конференция «Тихоновские чтения 2010», тезисы докладов (Москва, 25-29 октября 2010 г.). М.: Изд-во МАКС Пресс, 2010, С.9.
# О свойствах предполных классов в трехзначной логике // XI Межвузовский научно-практический семинар «Комбинаторные конфигурации и их применения» (Кировоград, 15-16 апреля 2011 г.), Материалы. Кировоград: Изд-во Кировоградского национального технического университета, 2011, С.117-122.
# О свойствах теоретико-множественных операций над предполными классами трехзначной логики // Проблемы теоретической кибернетики. Материалы XVI Международной конференции (Нижний Новгород, 20-25 июня 2011 г.). Нижний Новгород: Изд-во Нижегородского госуниверситета, 2011. C.336-340.
# О критериальной таблице в P_3 // Научная конференция «Ломоносовские чтения», тезисы докладов (Москва, 14-23 ноября 2011 г.). М.: Изд-во МАКС Пресс, 2011, С.27-29.
# О свойствах предполных классов в P_3 // Известия высших учебных заведений. Поволжский регион. Физ.-мат. науки. Пенза: Изд-во Пензенского государственного университета, 2012, №2 (22), C.16-24.
# О функциях четырехзначной логики, монотонных относительно линейных порядков // Материалы XIII Межвузовского научно-практического семинара «Комбинаторные конфигурации и их применения», (Кировоград, 13-14 апреля 2012 г.). Кировоград: Изд-во Кировоградского национального технического университета, C.107-109.
# О пересечениях классов монотонных функций многозначной логики // XI международный семинар «Дискретная математика и ее приложения», (Москва, 18-23 июня 2012 г.). М.: Изд-во механико-математического ф-та МГУ, С.207-209.
# О распределении трехзначных функций по предполным классам // Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика. 2012. № 3, С.45-52. (A.S.Nagornii "On the Distribution of Three-Valued Functions over Pre-Complete Classes", Moscow University Computational Mathematics and Cybernetics, 2012, Vol. 36, No.3, P.155-163) Allerton Press, Inc., 2012 (ISSN 0278-6419)
# О некоторых пересечениях предполных классов многозначной логики, вложенных в классы C_0 и C_{0,1,...,k-3} // Материалы Международного научного семинара «Дискретная математика и ее применение в экономико-математическом моделировании и информационных технологиях» (Запорожье, 11-13 октября 2012 г.). С.51-52;
# О некоторых пересечениях предполных классов многозначной логики // Научная конференция «Тихоновские чтения», тезисы докладов (Москва, 29-31 октября 2012 г.). М.: Изд-во МАКС Пресс, С.46-47.
# О линейной монотонности некоторых пересечений предполных классов многозначной логики // Материалы XV Международного научно-практического семинара «Комбинаторные конфигурации и их применения», (Кировоград, 12-13 апреля 2013 г.). Кировоград: ПП «Ексклюзив-Систем», C.75-78.
# О пересечениях и объединениях предполных классов многозначной логики // Научная конференция «Ломоносовские чтения» (Москва, 15-24 апреля 2013 г.) - М.: изд-во МАКС Пресс, 2013, С.13-15.
# Нагорный А.С. О ядровых аксиомах вложения в трехзначной логике // Матерiали III Всеукраïнського наукового семiнару «Комбiнаторна оптимiзацiя та нечiткi множини КОНеМ - 2013» (Полтава, 30-31 августа 2013 г.). Полтава: изд-во ПУЕТ, С.64-66.
# Intersections and embedding of intersections of M5 classes to some M5 classes // http://goo.gl/U42AeV, 2013.
# О свойствах пересечений предполных классов монотонных функций пятизначной логики // Научная конференция "Тихоновские чтения" (Москва, 28 октября -- 1 ноября 2013 г.), - М.: изд-во МАКС Пресс, 2013, С. 78.
# Intersections and embedding of intersections of U5 classes to some U5 classes // http://goo.gl/zALP1A, 2014.
# Нагорный А.С. О свойствах попарных пересечений предполных классов функций пятизначной логики, сохраняющих разбиения // Материалы XVI Международного научно-практического семинара «Комбинаторные конфигурации и их применения (11-12 апреля 2014 г.). Кировоград: Изд-во «Екслюзив-Систем», 2014, С. 108-111.
# О тривиальных пересечениях предполных классов пятизначной логики, сохраняющих разбиения // Научная конференция «Ломоносовские чтения» (Москва, 14-23 апреля 2014 г.), - М.: изд-во МАКС Пресс, 2014, С. 78-79.
# О свойствах пересечений предполных классов, сохраняющих разбиения, в пятизначной логике // Проблемы теоретической кибернетики. Материалы XVII международной конференции (Казань, 16-20 июня 2014 г.) – Казань: Изд-во Отечество, 2014, С.219-221.
# О свойствах монотонных самодвойственных функций четырехзначной логики // Научная конференция "Тихоновские чтения" (Москва, 27- 31 октября 2014 г.), - М.: изд-во МАКС Пресс, 2014, С.44.

Участник:FedorovaVS

2023-07-10T09:50:41Z

Root:

[[Категория:Сотрудники кафедры математической кибернетики (архив)]]

<div style="background-color: #FFAAAA; border-style: dotted">
'''Актуальность информации: 2013 год.'''

'''В настоящее время не является сотрудником кафедры.'''
</div>

'''Федорова Валентина Сергеевна''' - кандидат физико-математических наук, младший научный сотрудник. [[Image:Fedorova.png|thumb|right|Федорова Валентина Сергеевна]]

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

=== Функциональные уравнения многозначной логики ===
Исследование функциональных уравнений многозначной логики, в частности, свойств их решений в зависимости от используемых функциональных констант, оценок сложности проверки выполнимости таких систем, свойств нового оператора замыкания, определенного на их основе и порождающего конечную классификацию множества всех функций многозначной логики.

=== Структура замкнутых классов функций многозначной логики ===

=== Теория алгоритмического обучения ===

== Лекционные курсы ==
* [[Функциональные уравнения многозначной логики]]

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

== Избранные публикации ==
#С. С. Марченков, В. С. Федорова «О решениях систем функциональных булевых уравнений» ([[Media:DAIIO.pdf|pdf]])
#:{{Smaller|Дискретный анализ и исследование операций, 2008, том 15, № 6, с. 48-57.}}
#:
#С. С. Марченков, В. С. Федорова «О решениях систем функциональных уравнений многозначной логики» ([[Media:DAN.pdf|pdf]])
#:{{Smaller|Доклады Академии Наук, т. 426, № 4, 2009, с. 448-449.}}
#:
#С. С. Марченков, В. С. Федорова «Решения систем функциональных уравнений многозначной логики» ([[Media:Vestnik.pdf|pdf]])
#:{{Smaller|Вестник МГУ. Серия 15. Вычислительная математика и кибернетика. 2009. № 4. С. 29-33.}}
#:
#А. А. Вороненко, В. С. Федорова, Д. В. Чистиков «Повторность булевых функций в элементарном базисе» ([[Media:Kazan.pdf|pdf]])
#:{{Smaller|Известия вузов. Серия Математика. 2011, № 11, c. 72–77.}}
#:
#В. Б. Ларионов, В. С. Федорова «Надструктура классов самодвойственных k-значных функций» ([[Media:Irkutsk.pdf|pdf]])
#:{{Smaller|Известия Иркутского государственного университета. Серия Математика. 2011. Т. 4, № 3, с. 83-98.}}

{{DISPLAYTITLE:Федорова Валентина Сергеевна}}

Нагорный Александр Степанович

2023-02-19T18:31:58Z

Root:

#перенаправление [[Участник:NagornyAS]]
[[Категория:Сотрудники кафедры математической кибернетики (архив)]]

Категория:Сотрудники лаборатории ДУСП (архив)

2023-01-16T08:54:09Z

Root: Новая страница: «Бывшие сотрудники лаборатории дискретных управляющих систем и их приложений.»

Бывшие сотрудники лаборатории дискретных управляющих систем и их приложений.

Рамиль Альварес Хосе

2023-01-16T08:53:10Z

Root:

[[Категория:Сотрудники лаборатории ДУСП (архив)]]

'''Рамиль Альварес Хосе''' — кандидат физико-математических наук, ведущий научный сотрудник лаборатории ДУСП.

Данилов Борис Радиславович

2023-01-16T08:51:57Z

Root:

#REDIRECT [[Участник:DanilovB]]
[[КАТЕГОРИЯ:Сотрудники кафедры математической кибернетики]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

Файл:Verif VP 32.pdf

2022-12-11T20:08:57Z

Root: Методы верификации (618, 621). Блок 32. Решение BMC при помощи SAT

Методы верификации (618, 621). Блок 32. Решение BMC при помощи SAT

Половинкина Татьяна Ивановна

2022-03-10T17:38:47Z

Root: Новая страница: «Категория:Сотрудники лаборатории ДУСП Категория:Сотрудники кафедры МК и лаборатори…»

[[Категория:Сотрудники лаборатории ДУСП]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

'''Половинкина Татьяна Ивановна''' — инженер лаборатории ДУСП.

Рамиль Альварес Хосе

2022-03-10T17:36:35Z

Root: Новая страница: «Категория:Сотрудники лаборатории ДУСП Категория:Сотрудники кафедры МК и лаборатори…»

[[Категория:Сотрудники лаборатории ДУСП]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

'''Рамиль Альварес Хосе''' — кандидат физико-математических наук, ведущий научный сотрудник лаборатории ДУСП.

Владимирова Юлия Сергеевна

2022-03-10T17:35:15Z

Root: Перенаправление на Участник:VladimirovaYuS

#REDIRECT [[Участник:VladimirovaYuS]]
[[Категория:Сотрудники лаборатории ДУСП]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

Участник:VladimirovaYuS

2022-03-10T17:33:35Z

Root:

{{DISPLAYTITLE:Владимирова Юлия Сергеевна}}
'''Владимирова Юлия Сергеевна''' — кандидат физико-математических наук, старший научный сотрудник лаборатории ДУСП.

Участник:VladimirovaYuS

2022-03-10T17:33:24Z

Root: Новая страница: «{{DISPLAYTITLE:Бухман Антон Владимирович}} '''Владимирова Юлия Сергеевна''' — кандидат физико-ма…»

{{DISPLAYTITLE:Бухман Антон Владимирович}}
'''Владимирова Юлия Сергеевна''' — кандидат физико-математических наук, старший научный сотрудник лаборатории ДУСП.

Савицкий Игорь Владимирович

2022-03-10T17:32:09Z

Root: Перенаправление на Участник:SavitskiyIV

#REDIRECT [[Участник:SavitskiyIV]]
[[Категория:Сотрудники лаборатории ДУСП]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

Участник:SavitskiyIV

2022-03-10T17:30:24Z

Root: Новая страница: «{{DISPLAYTITLE:Савицкий Игорь Владимирович}} '''Савицкий Игорь Владимирович''' — кандидат физико…»

{{DISPLAYTITLE:Савицкий Игорь Владимирович}}
'''Савицкий Игорь Владимирович''' — кандидат физико-математических наук, инженер лаборатории ДУСП.

Ложкин Сергей Андреевич

2022-03-10T17:28:15Z

Root:

#перенаправление [[Участник:LozhkinSA]]
[[Категория:Сотрудники кафедры математической кибернетики]]
[[Категория:Сотрудники лаборатории ДУСП]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

Данилов Борис Радиславович

2022-03-10T17:26:50Z

Root:

#REDIRECT [[Участник:DanilovB]]
[[КАТЕГОРИЯ:Сотрудники лаборатории ДУСП]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

Бухман Антон Владимирович

2022-03-10T17:26:20Z

Root:

#REDIRECT [[Участник:BukhmanAV]]
[[Категория:Сотрудники лаборатории ДУСП]]
[[Категория:Сотрудники кафедры МК и лаборатории ДУСП]]

Участник:ShupletsovMS

2022-03-10T17:25:29Z

Root: уточнение должности

[[Image:Shupletsov.jpg|thumb|right|Шуплецов Михаил Сергеевич]]'''Шуплецов Михаил Сергеевич''' - кандидат физико-математических наук, доцент кафедры МК.
*e-mail: mikle.shupletsov@gmail.com
*[http://istina.msu.ru/profile/ShupletsovMS/ Профиль в системе ИСТИНА]

== [[Области научных интересов]] ==
* Дискретная математика
* Математическая кибернетика
* Теория анализа и синтеза дискретных управляющих систем
* Математические модели и методы автоматизации проектирования СБИС
* Математические модели в биологии

== Лекционные курсы ==
[[Математические модели и методы синтеза СБИС]]

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

* [[Некоторые вопросы теории управляющих систем]]
* [[Теория управляющих систем и математические модели СБИС]]

=== Ссылки ===
# M.S. Shupletsov, L.I. Golubeva, S.S. Rubina, D.A. Podvyaznikov, S. Iwatani, and S.V. Mashko. [http://www.microbialcellfactories.com/content/13/1/152 OpenFLUX2: 13C-MFA modeling software package adjusted for the comprehensive analysis of single and parallel labeling experiments]. Microbial Cell Factories, 13(1:152), 2014.
# Ложкин С.А., Шуплецов М.С. [http://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=uzku&paperid=1268&option_lang=rus О динамической активности схем из функциональных элементов и построении асимптотически оптимальных по сложности схем с линейной динамической активностью] // Ученые записки Казанского университета. Серия Физико-математические науки. — 2014. — Т. 156, № 3. — С. 84–97.
# Шуплецов М.С. [http://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=uzku&paperid=760&option_lang=rus Оценки высокой степени точности для сложности предикатных схем в некоторых базисах] // Ученые записки Казанского университета. Серия Физико-математические науки. — 2009. — Т. 151, № 2. — С. 173–184.

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

{{DISPLAYTITLE:Шуплецов Михаил Сергеевич}}

Участник:SeleznevaSN

2022-03-10T17:25:19Z

Root: уточнение должности

{{DISPLAYTITLE:Селезнева Светлана Николаевна}}
[[Image:Selezneva3.jpg|thumb|right|Селезнева Светлана Николаевна]]'''Селезнева Светлана Николаевна''' — доктор физико-математических наук, профессор кафедры МК,

e-mail: selezn@cs.msu.ru

[http://istina.msu.ru/profile/selezn@cs.msu.su Профиль Селезневой С.Н. в системе "ИСТИНА"]

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

*Дискретная математика

*Сложность алгоритмов

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

*Дискретные функции

Рассматриваются свойства дискретных функций и их представлений (полиномиальными и другими формами), разрабатываются алгоритмы нахождения оптимальных или близких к ним представлений дискретных функций.

*Графы и комбинаторика

Рассматриваются свойства графов и комбинаторных множеств и связанные с ними задачи.


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

*[[Сложность решения дискретных задач]]

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

*[[Дискретная математика (1-й поток)]] (обязательный курс для студентов 1-го курса, см. также [[Дискретная математика (1й курс)]])

*[[Избранные вопросы дискретной математики]] (обязательный курс для студентов 318 группы)

*[[Избранные вопросы теории графов]], часть 3 (обязательный курс для студентов 418 группы)

*[[Дискретные функции и выполнимость ограничений]] (обязательный курс для студентов 518/1 группы, спецкурс для студентов магистратуры)

*[[Дискретные модели]] (обязательный курс для студентов неинтегрированной магистратуры, 1-й курс)

*[[Графы и их приложения]] (спецкурс для аспирантов)

*[[Булевы функции и полиномы]] (спецкурс) - читался в 2008-2013 г.г.

==Учебные пособия==

[[Media:ok-2.pdf|Алексеев В.Б., Вороненко А.А., Ложкин С.А., Романов Д.С., Сапоженко А.А., Селезнева С.Н. Задачи по курсу "Основы кибернетики"]], 2-е изд. М.: МАКС Пресс, 2011.

[[Media:odm-selezn.pdf|Селезнева С.Н. Основы дискретной математики]]. М.: МАКС Пресс, 2010.

[[Media:bool_polynoms.pdf|Селезнева С.Н. Булевы функции и полиномы]]. Пособие по спецкурсу. Составители: Дайняк А.Б., Шуплецов М.С. Москва, 2006.

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

* аспиранты: Мельник Марина (4 г/о), Лю Юнцин (3 г/о), Лобанов Алексей (1 г/о)
* 618/1 группа: Шурыгин Дмитрий
* 518/1 группа: Мироненко Андрей, Вершков Станислав
* 418/1 группа: Бубнов Егор, Молдахметова Индира, Селевенко Роман
* 318 группа: Костиков Егор, Трофимов Арсений, Пак Анастасия, Сагандыкова Аида
* ВВО: Самсонов Михаил
* Ташкентский филиал: Рахимов Умархон

Участник:RomanovDS

2022-03-10T17:25:00Z

Root: уточнение должности

{{DISPLAYTITLE:Романов Дмитрий Сергеевич}}
[[Image:Romanov.jpg|thumb|right|Романов Дмитрий Сергеевич]]'''Романов Дмитрий Сергеевич''' — доктор физико-математических наук, доцент кафедры МК.

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

* Дискретная математика
* Математическая кибернетика
* Теория надежности
* Контроль управляющих систем

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

* [[Дискретная математика (1й курс)]]
* [[Избранные вопросы теории графов]]

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

* [[Некоторые вопросы теории управляющих систем]]
* [[Теория управляющих систем и математические модели СБИС]]

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

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

# Гаврилов Г.П., Романов Д.С. Методы линейной алгебры в теории графов (учебное пособие для студентов) // М.: Изд-во МГУ, 1996. — 72 с.
# О числе тупиковых проверяющих замыкания тестов для блочных контактных схем счетчиков четности. // Дискретная математика. — 1997. — Т. 9. Вып. 4. — С. 32-49.
# Об асимптотически минимальных единичных диагностических тестах для «прямоугольных» контактных схем, реализующих элементарные симметрические функции // Вестник Нижегородского государственного университета. Математическое моделирование и оптимальное управление. — 2000. — Вып. 1(22). — С. 159-167.
# Об оценках функций Шеннона длины единичных тестов относительно транспозиций переменных // Вестн. Моск. ун-та. Сер. 15. Вычисл. матем. и киберн. — 2007, № 2. — С. 23-29.
# Кузнецов И.А., Романов Д.С. О полных проверяющих тестах относительно локальных слипаний переменных в булевых функциях // Ученые записки Казанского университета. Серия Физико-математические науки. — 2009 г. — Том 151, книга 2. — Стр. 90-97.
# D.S. Romanov. Diagnostic tests for local coalescences of variables in Boolean functions // Computational Mathematics and Modeling, Vol. 23, No 1, January, 2012, pp. 72-79.
# Метод синтеза легкотестируемых схем в одном базисе, допускающих единичные проверяющие тесты константной длины // Вестн. Моск. ун-та. Матем. Механ. — 2012. № 2. — С. 24-29.
# Романов Д.С., Антюфеев Г.В. О тестах относительно примитивных сдвигов переменных в булевых функциях // Вопросы радиоэлектроники. Серия «Электронная вычислительная техника». 2013. Вып. 2. С. 64-68.
# D.S. Romanov. Tests with respect to permutations of variables in Boolean functions // Computational Mathematics and Modeling, Vol. 24, Issue 4, October, 2013, pp. 558-565.
# О синтезе схем, допускающих полные проверяющие тесты константной длины относительно произвольных константных неисправностей на выходах элементов // Дискретная математика. — 2013. — Т. 25, вып. 2. — С. 104-120.
# Метод синтеза легкотестируемых схем, допускающих единичные проверяющие тесты константной длины // Дискретная математика. — 2014. — Т. 26, вып. 2. — С. 100-130.
# О синтезе контактных схем, допускающих короткие проверяющие тесты // Ученые записки Казанского университета. Серия Физико-математические науки. — 2014. — Т. 156. Кн. 3. — С. 110-115.

Участник:PodymovVV

2022-03-10T17:24:45Z

Root: уточнение должности

{{DISPLAYTITLE:Подымов Владислав Васильевич}}
[[Image:Podymov.jpg|thumb|right|Подымов Владислав Васильевич]]'''Подымов Владислав Васильевич''' — кандидат физико-математических наук, доцент кафедры МК.

* e-mail: valdus@yandex.ru
* [http://istina.msu.ru/profile/pellman/ Профиль в системе ИСТИНА]

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

* Формальная верификация программ и цифровой аппаратуры
* Проверка эквивалентности программ
* Программно-конфигурируемые сети
* Временные автоматы

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

* [[Математическая логика (группы 318, 241)]]
* [[Математические методы верификации схем и программ]]
* [[Математические модели и методы проектирования архитектуры сверхбольших интегральных схем]]
* [[Языки описания схем]]

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

* [[Теоретические проблемы программирования]]