model-checking

model-checking@asvk.cs.msu.ru

130 обсуждения

Подведение итогов по первому заданию
by model checking course mailing list 05 Мар '11

05 Мар '11

Дорогие студенты, Дедлайн по первому заданию прошёл. 6 человек из сдавших на семинаре до сих пор не прислали копии на почту (у вас есть время до 14.03). Работы, просто присланные на почту до 02.03 включительно (не сданные на семинаре) будут проверены со временем. 17 человек не сдавали работы на семинаре и не прислали их на почту. Вы можете сдать их _только_ на семинаре, до 14 марта включительно, число баллов будет умножено на 0.6. 14 марта списки не приступивших к практикуму студентов будут у Березина. В отличие от прошлого года, результаты проверки на плагиат радуют -- в паре обнаруженных случаях совместного творчества соавторы постарались сделать программы непохожими не просто переименованием переменных, но и вынесением функций, изменением порядка вычисления состояний и другими интересными способами, демонстрирующими по крайней мере понимание того, что делает программа. Приложенные усилия стоят того, чтобы не считать это плагиатом :-) К.

1 0

Копии сданных заданий
by model checking course mailing list 27 Фев '11

27 Фев '11

Дорогие студенты, Напоминаю, что копии сданных на семинаре заданий необходимо прислать на адрес model-checking(a)lvk.cs.msu.su. С уважением, Константин Савенков.

1 0

Опции компилятора
by model checking course mailing list 17 Фев '11

17 Фев '11

Дорогие студенты, Как многие из вас заметили, не все указанные в требованиях к решению параметры командной строки компилятора применимы для языка С++. Такие параметры при компиляции программы на С++ можно (и нужно) опускать. С уважением, Константин Савенков.

1 0

Re: [model-checking] Model Checking Task 1
by model checking course mailing list 16 Фев '11

16 Фев '11

Здравствуйте, Давайте для АСВК сделаем последним днём сдачи 2 марта. 2 марта задание можно будет сдавать только на семинаре, сдача по почте -- до 28 февраля включительно. С уважением, Константин Савенков. On 2/16/11 6:15 PM, Русланова Анна wrote: > Добрый день, > Скажите, пожалуйста, как студентам кафедры АСВК в срок сдать задание > по практикуму? Занятия у нас в среду. До этой среды мало кто успел > сделать задание, а следующая среда - праздник 23 февраля. Окончание > сдачи по вашим словам 28 февраля. > С уважением, > Русланова Анна, студентка 421 группы.

1 0

Список рассылки и практикум
by model checking course mailing list 12 Фев '11

12 Фев '11

Дорогие студенты, Со следующей недели начинается практикум, занятия по расписанию. Сейчас прислали свои почтовые адреса 57 человек из 119 на курсе (см. https://spreadsheets.google.com/pub?key=0AhbmHMR5VBIJdDFHTW1ZZGxmaF93M3ViOF… <https://spreadsheets.google.com/pub?key=0AhbmHMR5VBIJdDFHTW1ZZGxmaF93M3ViOF…>). Большая просьба -- попросите старост своих групп напомнить всем, что нужно подписаться на список рассылки до вечера воскресенья. Те, кто не подписался, не получат вовремя первое задание по курсу. Если это сообщение читают старосты и у них есть списки адресов группы -- можете прислать их мне, я подпишу всю группу. Спасибо, с уважением, Константин Савенков.

1 0

Re: [model-checking] Пересдача 15 сентября
by model checking course mailing list 10 Сен '10

10 Сен '10

Ну да, да. 15 сентября, в среду. С уважением, Константин Савенков. 10.09.2010 16:30, Alexander Fingerov пишет: > model checking course mailing list <model-checking(a)lvk.cs.msu.su> > писал(а) в своём письме Fri, 10 Sep 2010 15:51:04 +0400: >> 9 сентября, в понедельник, будет пересдача. Время начала -- 11 утра, >> аудитория 505. > > Мне кажется, всё-таки не 9 сентября и не в понедельник :) >

1 0

Пересдача 15 сентября
by model checking course mailing list 10 Сен '10

10 Сен '10

Дорогие студенты, 9 сентября, в понедельник, будет пересдача. Время начала -- 11 утра, аудитория 505. Тем, у кого максимальный возможный балл не превышает 2, будет предложена контрольная работа. В работе будет набор простых задач, проверяющих те практические навыки, которые вы должны были получить в ходе данного курса, а именно: 1. Оценка числа потенциальных состояний параллельной программы, 2. Оценка числа достижимых состояний параллельной программы, 3. Построение LTS 4. Построение модели параллельной программы на языке Promela, 5. Выполнение абстракции с учётом проверяемых свойств, 6. Формулировка свойств параллельной программы при помощи встроенных средств SPIN, 7. Формулировка свойств параллельной программы при помощи LTL, При выполнении всех заданий (с незначительными недочётами) у вас будет базовый балл 0, максимальная оценка 3 и возможность сдать устный экзамен. В остальном пересдача будет протекать по той же схеме, что и основной экзамен. Распорядок сделаем такой: все приходят к 11, с 11 до 13 те, кому это нужно, пишут контрольные, в это время готовятся и сдают остальные. Дальше мы сделаем небольшой перерыв для проверки контрольных, после которого примем устный экзамен у тех "подконтрольных", кому имеет смысл его сдавать. На всякий случай напоминаю всем про недопустимость использования на экзамене шпаргалок, мобильных телефонов и иных заменителей памяти. С уважением, Константин Савенков.

1 0

Пересдача 21.06
by model checking course mailing list 19 Июн '10

19 Июн '10

Дорогие студенты, 21 июня, в понедельник, будет пересдача для тех из вас, кто не уехал на военные сборы. Время начала -- 10 утра, аудитория 510. Тем из вас, кто попал на пересдачу "автоматом" из-за пробивания практикума, будет предложена контрольная работа. В работе будет набор простых задач, проверяющих те практические навыки, которые вы должны были получить в ходе данного курса, а именно: 1. Оценка числа потенциальных состояний параллельной программы, 2. Оценка числа достижимых состояний параллельной программы, 3. Построение модели параллельной программы на языке Promela, 4. Выполнение абстракции с учётом проверяемых свойств, 5. Формулировка свойств параллельной программы при помощи встроенных средств SPIN, 6. Формулировка свойств параллельной программы при помощи LTL, ну и заодно 7. Построение автомата Бюхи по формуле LTL. При выполнении всех заданий (с незначительными недочётами) у вас будет базовый балл 0, максимальная оценка 3 и возможность сдать устный экзамен. В остальном пересдача будет протекать по той же схеме, что и основной экзамен. Для тех, кто в танке, сообщаю, что после начала подготовки и до выставления оценки 1) общение с сокурсниками 2) пользование мобильным телефоном и 3) использование шпаргалок запрещено и ведёт к удалению с экзамена с выставлением оценки "неудовлетворительно". Выход из аудитории во время экзамена сопровождается сдаванием работы. С уважением, Константин Савенков.

1 0

Оценки и время экзамена
by model checking course mailing list 07 Июн '10

07 Июн '10

Дорогие студенты, Поскольку на консультации было довольно мало народа, напишу на всякий случай сюда. Оценка складывается из следующих частей: - задача на LTL; необходимо построить формулу, а при ответе сказать, на каких классах трасс выполняется/не выполняется свойство и обосновать, почему это так, опираясь на структуру формулы; правильное решение оценивается в 0,5 балла, неправильное -- в -0,5 за попытку, всего две попытки, тем самым вы получаете -1..+0,5 - два вопроса -- за каждый 0..1 балла - один обязательный дополнительный вопрос: 0 (пусть будет так)..0,5 Далее дополнительные вопросы (скорее всего, по ненаписанным контрольным), если принимающий сочтёт это необходимым. Каждый вопрос -- -0,5 (неверный ответ) или +0,5 (верный ответ). В табличке указано, во сколько вам приходить -- обратите внимание, пожалуйста. С уважением, Константин Савенков.

1 0

Не сдавшим комиссию
by model checking course mailing list 24 Май '10

24 Май '10

Четверо человек с АСВК, не сдавших комиссию -- 27-го мая в 11:00 найдите Игоря Коннова в районе к.764 и попробуйте ещё раз. На первый экзамен, впрочем, можете не приходить. С уваженем, Константин Савенков.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking