ВПнМ

Материал из eSyr's wiki.

(Различия между версиями)
Перейти к: навигация, поиск
(Практикум и зачёт курса)
(Практикум и зачёт курса)
Строка 26: Строка 26:
* Дана одна из функций ОС Minix, необходимо построить её модель ([[ВПнМ, примеры задач/Задача 3|пример задачи]]).
* Дана одна из функций ОС Minix, необходимо построить её модель ([[ВПнМ, примеры задач/Задача 3|пример задачи]]).
* Для модели, построенной в предыдущей задаче, проверить ряд свойств ([[ВПнМ, примеры задач/Задача 4|пример задачи]]).
* Для модели, построенной в предыдущей задаче, проверить ряд свойств ([[ВПнМ, примеры задач/Задача 4|пример задачи]]).
-
* Задачи на LTL (([[ВПнМ, примеры задач/Задача 5|примеры задач]]).
+
* Задачи на '''LTL''' ([[ВПнМ, примеры задач/Задача 5|примеры задач]]).
Экзамен:
Экзамен:
-
* Экзамен устный
+
* Экзамен устный, принимает ~3 экзаменатора.
-
* Кто пришлёт в течении одной-двух недель письмо, получит задачу, а также, если решит её в течении одной-двух недель, не получит задачу на экзамене
+
* '''Те, кто на протяжении семестра работал и за все сданные задачи получен полный балл, может получить "3" автоматом'''.
-
* Для тех, кто решит все задачи будет проведён предварительный экзамен на гуманных условиях
+
* (тем, кто сдает Савенкову): '''без решённой LTL оценка за экзамен поставлена не будет'''.
== Литература ==
== Литература ==

Версия 18:30, 24 мая 2009

Савенков Константин Олегович
Савенков Константин Олегович

Содержание

Информация о курсе

Структура курса

  • Моделирование последовательных программ и параллельно взаимодействующих систем
  • Спецификация проверяемых свойств
  • Верификация при помощи Spin
  • Алгоритмы верификации
  • Теоретические и практические трудности верификации

Практикум и зачёт курса

Список задач (примеры задач):

  • Дана программа, необходимо посчитать количество потенциальных и достижимых состояния, а так же построить LTS-диаграмму (пример задачи). Срок сдачи — до 23 марта.
  • Для программы из первого задания построить её модель с использованием системы SPIN, а также вычислить с её использованием количество состояний модели. В качестве решения прислать модель и output верификатора (пример задачи).
  • Дана одна из функций ОС Minix, необходимо построить её модель (пример задачи).
  • Для модели, построенной в предыдущей задаче, проверить ряд свойств (пример задачи).
  • Задачи на LTL (примеры задач).

Экзамен:

  • Экзамен устный, принимает ~3 экзаменатора.
  • Те, кто на протяжении семестра работал и за все сданные задачи получен полный балл, может получить "3" автоматом.
  • (тем, кто сдает Савенкову): без решённой LTL оценка за экзамен поставлена не будет.

Литература

  • Кларк, Грамберг, Пелед. Верификация моделей программ: Model checking, МЦНМО, 2002
  • Holzmann. The Spin Model Checker: Primer and Reference Manual, Addison Wesley, 2003

Ссылки

Курс


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


01 02 03 04 05 06 07 08 09 10


Календарь

пт пт пт пт пт
Февраль
  08 15 22 29
Март
  14 21 28
Апрель
04 11 18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин


Лекции

10 семестр История развития вычислительных технологий в СССР, России | Современные проблемы прикладной математики
9 семестр Формальная спецификация и верификация программ | Теория игры и исследования операций | История и методология прикладной математики | Основы российского права | История религии | Параллельная обработка данных
8 семестр Верификация программ на моделях | Математические основы теории прогнозирования | Основы квантовой физики и квантовых вычислений | Методы оптимизации | Распределённые операционные системы
7 семестр Вычислительные Системы | Объектно-ориентированные Анализ и Проектирование | Искусственный Интеллект | Математическая Логика | Функциональный Анализ | Социология | Параллельная Обработка Данных
6 семестр Основы Кибернетики | Численные Методы | Конструирование Компиляторов | Компьютерные Сети
5 семестр Базы Данных | Языки Программирования | Экономические Науки
3 семестр Операционные системы

Спецкурсы
Осень 2013 Современная криптография | Дизайн и реализация ОС FreeBSD
Весна 2011 Практические аспекты сетевой безопасности | Сетевое администрирование в UNIX
Осень 2010 UNИX | Теория функционального программирования. Язык Haskell | Введение в информационную безопасность | Информационный поиск
Весна 2010 UNИX | Архитектура и программирование массивно-параллельных вычислительных систем | Язык Ада
Осень 2009 UNИX | Введение в парадигмы программирования
Весна 2009 UNИX | Архитектура и программирование массивно-параллельных вычислительных систем
Осень 2008 UNИX | Структурные методы обработки изображений и сигналов
Весна 2008 UNИX | Вопросы организации вычислительных кластеров на основе UNIX-серверов | Философия математики
Осень 2007 UNИX
Весна 2007 UNИX | Практика мультипарадигмального программирования
Осень 2006 Введение в теорию построения оптимизирующих компиляторов

Отдельные лекции Bruce Eckel, The State of The Java Union | Richard Stallman: Free software: ethics and practice, Copyright vs Community in the Age of Computer Networks | Наану Александр, Vim | Erinn Clark, The Tor Project: Anonymity Online
Личные инструменты
Разделы