Курс «Верификация моделей программ»

Лектор: Камкин Александр Сергеевич — ассистент кафедры, канд. физ.-мат. наук, ведущий научный сотрудник Института системного программирования РАН им. В.П.Иванникова.
Семестр: весенний.
Аудитория: магистранты программы «Технологии программирования» (может быть выбран в качестве элективного курса магистрантами других программ).

Аннотация

Лекционный курс с экзаменом, семинарами и практическими заданиями. В курсе рассматриваются моделирование программ и формализация требований, спецификация и верификация параллельных программ, язык Promela и инструмент проверки моделей Spin, моделирование программ структурами Крипке, автоматы Бюхи и omega-регулярные языки, дополнительные вопросы верификации моделей программ.

Учебное пособие

Камкин А.С. Введение в формальные методы верификации программ: учебное пособие / А.С. Камкин. — Москва: МАКС Пресс, 2018. — 272 с.
Скачать пособие (pdf)
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации требований (программные контракты и темпоральная логика линейного времени), методы доказательства корректности программ (метод индуктивных утверждений и метод фундированных множеств) и методы проверки моделей (теоретико-автоматный подход в явной и символической формах). В пособии также затрагиваются вопросы абстрактной интерпретации, разрешения ограничений, применения формальных методов в тестировании; даются сведения об инструментах Frama-C и Spin. Каждая глава сопровождается примерами и упражнениями.
Пособие предназначено для студентов и аспирантов программистских специальностей, а также преподавателей и исследователей в области информатики и программной инженерии.

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

© Кафедра системного программирования ВМК МГУ.

Обновлено: 5.3.2018