МФСП

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

(Различия между версиями)
Перейти к: навигация, поиск
м
Текущая версия (02:43, 26 декабря 2010) (править) (отменить)
(+2010)
 
(6 промежуточных версий не показаны.)
Строка 2: Строка 2:
[[Image:Petrenko.jpg|240px|thumb|Петренко Александр Константинович]]
[[Image:Petrenko.jpg|240px|thumb|Петренко Александр Константинович]]
-
[[Image:Petrenko_bot.jpg|240px|thumb|]]
+
[[Image:Petrenko_bot.jpg|240px|thumb|Алексей Хорошилов]]
== Информация о курсе ==
== Информация о курсе ==
* Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru)
* Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru)
Строка 8: Строка 8:
* Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя.
* Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя.
-
* Для оценки нужно иметь зачёт по практикуму, суммарная оценка на экзамене складывается из оценки на коллоквиуме, на экзамене и, возможно, оценке за практикум
+
* Для оценки нужно иметь зачёт по практикуму, суммарная оценка на экзамене складывается из оценки на коллоквиуме, на экзамене и, возможно, оценки за практикум
== Структура курса ==
== Структура курса ==
Строка 16: Строка 16:
# (3—4 лекции) Инструментальная поддержка аналитической верификации. В качестве базы испльзуется PVS
# (3—4 лекции) Инструментальная поддержка аналитической верификации. В качестве базы испльзуется PVS
# Коллоквиум
# Коллоквиум
-
# Экзамен
+
# Экзамен (результаты: [http://spreadsheets.google.com/pub?key=tACFiixUTF7fD4j7Sj3oUnQ&gid=2 2009] [https://spreadsheets.google.com/pub?key=0AoN5iJE0CvIadGV1NjdOQjV0eXdsSEpoRVZ5TFBoNHc&hl=ru&output=html 2010])
== Материалы ==
== Материалы ==
Строка 23: Строка 23:
* [http://sp.cs.msu.su/courses/fmsp/total13.zip [Кузьменкова, Петренко-1999] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму]
* [http://sp.cs.msu.su/courses/fmsp/total13.zip [Кузьменкова, Петренко-1999] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму]
* [http://sp.cs.msu.su/courses/fmsp/msc&sdl.pdf [Мансуров, Майлингова] Мансуров Н. Н., Майлингова О. Л. "Методы формальной спецификации программ: языки MSC и SDL" Методическое пособие по практикуму]
* [http://sp.cs.msu.su/courses/fmsp/msc&sdl.pdf [Мансуров, Майлингова] Мансуров Н. Н., Майлингова О. Л. "Методы формальной спецификации программ: языки MSC и SDL" Методическое пособие по практикуму]
-
(см. также Ссылки)
 
-
== Ссылки ==
+
=== Ссылки ===
* [http://sp.cs.msu.su/courses/fmsp/ Страница курса на сайте кафедры СП]
* [http://sp.cs.msu.su/courses/fmsp/ Страница курса на сайте кафедры СП]
* [http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/RMain.html Страница курса на сайте ИСП РАН]
* [http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/RMain.html Страница курса на сайте ИСП РАН]
Строка 36: Строка 35:
* [http://www.google.com/search?q=Microsoft+Interoperability+Project Microsoft Interoperability Project]
* [http://www.google.com/search?q=Microsoft+Interoperability+Project Microsoft Interoperability Project]
* [http://www.google.com/search?q=PVS+Specification+and+Verification+System PVS], [http://www.google.com/search?q=Isabelle+theorem+prover Isabella], [http://www.google.com/search?q=HOL+theorem+prover HOL]
* [http://www.google.com/search?q=PVS+Specification+and+Verification+System PVS], [http://www.google.com/search?q=Isabelle+theorem+prover Isabella], [http://www.google.com/search?q=HOL+theorem+prover HOL]
 +
 +
== Курс ==
 +
* [[МФСП: Оформление задач|Оформление задач]]
{{Курс МФСП}}
{{Курс МФСП}}
 +
{{Лекции}}

Текущая версия

Содержание

[править] Формальная спецификация и верификация программ

Петренко Александр Константинович
Петренко Александр Константинович
Алексей Хорошилов
Алексей Хорошилов

[править] Информация о курсе

  • Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru)
  • Семинарист АСВК — Петровский Михаил Игоревич
  • Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя.
  • Для оценки нужно иметь зачёт по практикуму, суммарная оценка на экзамене складывается из оценки на коллоквиуме, на экзамене и, возможно, оценки за практикум

[править] Структура курса

  1. (5—6 лекций) RAISE/RSL
    • (~3 семинара) Параллельно с этим нач. практические занятия. Порядка трёх занятий на практикуме будет посвящено выполнению и сдаче контрольных заданий на практикуме
  2. (3 лекции) Методы аналитической верификации. В частности, метод Флойда
  3. (3—4 лекции) Инструментальная поддержка аналитической верификации. В качестве базы испльзуется PVS
  4. Коллоквиум
  5. Экзамен (результаты: 2009 2010)

[править] Материалы

[править] Ссылки

«Что гуглить»:

[править] Курс


Формальная спецификация и верификация программ


Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14


Календарь

Сентябрь
03 10 17 24
Октябрь
01 08 15 22 29
Ноябрь
12 19 26
Декабрь
03 17
Семинары

01 02 03 04 05 06


Календарь

Сентябрь
01 08 15 22 29
Октябрь
06

Оформление задач|Проведение экзамена


Лекции

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
Личные инструменты
Разделы