ВПнМ

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: Савенков Константин Олегович == Информация о курсе == * Лектор — Савенков К...)
Строка 15: Строка 15:
Какие задачи:
Какие задачи:
* Будет дана программы, оценить кол-во состоянии, потом при помощи spin
* Будет дана программы, оценить кол-во состоянии, потом при помощи spin
-
* Задачи на моделирование рпограмм: построить модель и прогнать на имит. движке: Minix или Plan9
+
* Задачи на моделирование программ: построить модель и прогнать на имит. движке: Minix или Plan9
* Планируется дать более сложную задачу, задача чуть побольше
* Планируется дать более сложную задачу, задача чуть побольше
Экзамен:
Экзамен:

Версия 22:50, 23 февраля 2008

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

Содержание

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

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

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

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

Какие задачи:

  • Будет дана программы, оценить кол-во состоянии, потом при помощи spin
  • Задачи на моделирование программ: построить модель и прогнать на имит. движке: Minix или Plan9
  • Планируется дать более сложную задачу, задача чуть побольше

Экзамен:

  • Экзамен устный
  • Кто пришлёт в течении одной-двух недель письмо, получит задачу, а также, если решит её в течении одной-двух недель, не получит задачу на экзамене
  • Для тех, кто решит все задачи будет проведён предварительный экзамен на гуманных условиях

Литература

  • Кларк, Грумберг, Пелед. Верификация моделей программ: 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
Получено с http://esyr.name/wiki/%D0%92%D0%9F%D0%BD%D0%9C
Личные инструменты
Разделы