model-checking

model-checking@asvk.cs.msu.ru

130 обсуждения

Порядок сдачи экзамена
by model checking course mailing list 22 Июн '13

22 Июн '13

Дорогие студенты, Для тех из вас, кто не был на консультации, сообщаю, как будет проходить экзамен. Экзамен письменный. На экзамене вы получите следующие вопросы (в скобках указан диапазон баллов, которые можно получить за ответ на вопрос - [fail,win]): - вопрос из первой половины списка вопросов [0..1] - вопрос из второй половины списка вопросов [0..1] - дополнительный вопрос [0..0.5] - задача на LTL [-0.5..0.5] - по одному дополнительному вопросу [-0.5..+0.5] за каждую контрольную, за которую в семестре вы получили -1 (вопрос по тематике контрольной) Да, при очень плохом ответе можно получить оценку меньше базового балла. Да, базовый балл можно проставить в зачетку, не сдавая экзамена (хотя я не рекомендую). Время на написание ответов - 2 часа. Пользоваться можно только ручкой и головой, бумагу вам выдадут. Телефоны, вещи и разные полезные гаджеты остаются при входе в аудиторию. Во время написания ответов консультироваться с другими студентами нельзя, списывать также нельзя. Выход из аудитории сопровождается сдаванием работы. Нарушение этих правил влечет удаление с экзамена и выставление оценки неуд. Мы постараемся проверить работы в тот же день и выложить комментарии. Проставление оценок будет проходить в дополнительный день после экзаменов (или на последующих экзаменах других групп). Аппеляции -- строго в отдельный день. Студенты с базовым баллом -1 приглашаются сразу не пересдачу. С уважением, Константин Савенков.

1 0

Комиссия по верификации
by model checking course mailing list 11 Июн '13

11 Июн '13

Дорогие студенты, В четверг пройдет комиссия по практикуму, с 10:30 и до последнего человека (но не позже 18:30) в комнате 758а. На комиссии те (и только те), у кого в таблице стоит 2 балла за практикум, смогут, сдав все задания, исправить 2 на 3. Пожалуйста, не забудьте ведомости комиссии для АСВК. С уважением, Константин Савенков.

1 1

Зачет и экзамены
by model checking course mailing list 24 Май '13

24 Май '13

Дорогие студенты, ПРАКТИКУМ Вчера был "зачет" по курсу, все кто хотел досдали практикум. Зачетные ведомости для АСВК ушли в учебную часть. Зачет был с оценкой, при выставлении оценки я достаточно сильно округлял вверх - но учтите, что на базовый балл это округление не влияет. Несколько человек не получили зачет в силу того, что даже с округлением не набрали на 3 балла (см. в таблице). Скорее всего, для вас на следующей неделе будет комиссия. Как только мне сообщат из учебной части, мы это организуем. Несколько человек не получили зачет в зачетку - вы сможете сделать это на комиссии. На комиссии нужно будет полностью сдать все несданные задания практикума. За это будет выставлено 3 балла (=> на экзамене базовый балл 1) Далее. Есть люди не с АСВК, получившие 2 балла за практикум. Я предлагаю вам также придти на комиссию и повысить свой базовый балл до 1, сдав все задания практикума. АВТОМАТЫ В таблице указано, кто можнет получить оценку "отлично" автоматом (= базовый балл 4). Те, у кого базовый балл = 3, также могут автоматом проставить "3" за экзамен, но я рекомендую попробовать сдать экзамен. Проставить оценки в зачетные книжки можено будет во время комиссии по практикуму на следующей неделе или во время основного экзамена. ДОСРОЧНЫЙ ЭКЗАМЕН К сожалению, достаточно небольшой группы студентов для досрочного экзамена я не вижу. Если кому-то нужен досрочный экзамен в силу того, что у вас сборы итп - напишите мне, мы сделаем так, что вы напишете экзаменационную работу во время комиссии по практикуму на следующей неделе. С уважением, Константин Савенков.

1 0

Прием практикума
by model checking course mailing list 23 Май '13

23 Май '13

Дорогие студенты, Сейчас (14:60) осталось сдавать пятое задание примерно 8 человек. Как только сдаст последний, прием будет прекращен. Поэтому, если вы все же планируете сегодня сдавать практикум, бегите быстрее в МЗ-4. Я буду на ф-те до 17:00 в к 761. С уважением, Константин Савенков.

1 0

Прием 5-го задания практикума в зачетную сессию
by model checking course mailing list 15 Май '13

15 Май '13

Дорогие студенты, День в зачетную сессию - 23 мая, четверг, МЗ-4 забронирован на все пять пар. С уважением, Константин Савенков.

1 0

Семинары 15.05
by model checking course mailing list 14 Май '13

14 Май '13

Дорогие студенты, Семинаров 15.05 не состоится, поскольку у всех ведущих семинары - экзамен по философии. Все, кто не успеет из-за этого что-то сдать, смогут сделать это в выделенный день в зачетную сессию. Что это за день - напишу чуть позже. С уважением, Константин Савенков.

1 0

Model Checking Task 5
by model checking course mailing list 06 Май '13

06 Май '13

??? ?????? ? ??????? ??????? ????????? ? ??????????? ??? ??? ??????: 1. ????????? ???????? ?????????? ??????? (invalid end-states). ??????? ? ?????? ???? ?? ??????. ????? ???????????? ?? ???????? ???????? ????????? ? ????????? ???? ? ?????? task5_safety_out.txt. 2. ? ?????? ?? ?????? ???? ????????????? ???? (unreachable code), ?? ??????????? ???????? ????????? ????????? (-end-). ???? ????? ??? ? ?????? ??????, ????????? ??. 3. ? ?????? ?? ?????? ???? ?????? ??????????? (non-progress cycles), ?? ???????????: 3.1) ?????, ?????????? ? ??????????? ??????????? ???????????? ??????? 3.2) ??????, ??????????????? ?????? ???????????? ???????, ??????? ????? ?????????? ?????????? ????? ????????????. ????? ???????, ???????????, ??????????? ? ?????? (????????, ??????????????? ??? ????????????? ????????? ??????) ?? ?????? ??????? ? ?????? ??????????? ??????. ????? ???????????? ??? ???????? ?????????? ?????? ??????????? ????????? ? ????? ? ?????? task5_nonprogress_out.txt. ????? progress, ??????????????? ??? ????, ????? ??????????? ?? ??????? ???????? ?? ??????????? ?????, ????????????? ? ??????? 3.1 ? 3.2, ?????? ???? ??????????? ? ?????? model_assert.pml. 4. ????????????? ???? ???????? ??????? ? ??????? ?????? ????????? ??????? ? ??????? Spin, ????????? ? ??????? Spin. ??? ???? ?? ?????? ?????????????? ?????-???? ??????????????? ??????????. ???????????? ????????? ? ????? ? ??????? spec.ltl: 4.1. ? ???? ?????????? ???? ??????? ???? ??? ?????? ?????????? ??????? ??????? ??????? ??? ?????? ?????????? ??????*alloc*. 4.2. ? ???? ?????????? ???? ??????? ????? ????????? ??????? ??????? ???? ??? ?????? ?????? ????????????? ??? ?????? ??????*free*, 4.3. ?? ?????? ????? ????????? ??????? ????????? ? ???????????? ??????? ??????????? ???????? ?????? ?? ????????? ????????. 4.4. ? ??????????? ?????? (????? ???????? spin_lock* ? spin_unlock*) ????? ?????????? ?? ????? ?????? ????????. 4.5. ? ???? ?????????? ???? ???????, ??????? kfree ?????????? ?? ????? ?????? ????. ????????, ??? ???????? ???????? ??????? ?????? ???????? ????????: ????????? ??????, ???????? ??????? ???????????, ???????? ????????? ??????, ?? ???????? ? ??????, ??-??????? ??????? ???????? ??????? ? ??????????? ?????? ???. 5a. ? ??????, ???? ?????? ???????? ????????: - ???????, ?????? ???????????? ?? ??????????? ?? ???????? ??????; - ???????, ??? ?????????? ?????? ? ??????; - ???????, ?????? ????? ?????? ?????????; - ????????? ???????????, ???????? pan, ? ????? counterexample.txt; - ????????? ???????? ? ?????????? ?????? ? ?????? task5.pml ? task5_modified.pml; - ????????? ????? pan ? ????? task5_ver_out.txt. 5b. ? ??????, ???? ???????????? ?? ??????????? ?? ??????: - ????????? ???????????, ???????? pan, ? ????? counterexample.txt; - ????????? ?? ???????????? Spin ??????????? ?? ???????? ?????????; - ????????? ? ???, ??? ??????????? ?? ???????? ????????? ???????????; - ????????? ??????????? ?? ???????? ????????? ? ????? prog_counterexample.txt. ??????????? ?????? ???? ?????? ? ???? ?????????????????? ??????? ????? ???????? ????????? ? ???????? ??????????. - ????????? ?????? ? ????? task5.pml; - ????????? ????? pan ? ????? task4_ver_out.txt. - ??????? ??????????????? ???? ?? ????????????? (????????, «spec_1.ltl») ??? ???????? ?????????? ???????. 5c. ? ??????, ???? ????????? ? ?????? ?? ????????????? ? ???????????? ???????????: - ????????? ?????? ? ????? task4.pml; - ????????? ????? pan ? ????? ver_out.txt. ??????e ????? ????? -- "????????" ???? ? ???????? ?????? (?????????? ???? ?????? ?????). ??????? ?? ????????? ? ?????? ?????? ?? ?????, ?? ???? ?? ?? ??????? ???????/????? ??????? ? ????? ????????? ???, ????? ????? ?? ??????????? ??????? ???????. ? ?????????, ?????????? ????????.

1 0

Re: [model-checking] Лекция 6.05.13
by model checking course mailing list 06 Май '13

06 Май '13

Дорогие студенты, Простите, если кто-то пришел в пустую аудиторию, я полагал, что в конце прошлой мы обсудили - следующая будет после праздников. Соответственно, она будет 13-го мая. Будет контрольная по последней лекции, а затем я кратко пройдусь по всему курсу. С уважением, Константин Савенков. On 5/6/13 12:55 AM, Валерий Бицоев wrote: > Здравствуйте! > Я слегка запутался, слышал противоречивые мнения, подскажите > пожалуйста, будет ли завтра(06.05.13) лекция/консультация по > верификации на первой паре? > > -- > С уважением, > Бицоев Валерий

1 0

Семинары 6 мая
by model checking course mailing list 29 Апр '13

29 Апр '13

Дорогие студенты, Не волнуйтесь, семинары 6 мая пройдут по расписанию. С уважением, Константин Савенков.

1 0

Отмена лекции 15.04
by model checking course mailing list 13 Апр '13

13 Апр '13

Дорогие студенты, Лекции в следующий понедельник, 15 апреля, не будет - я в командировке. Следующая лекция состоится 22 апреля. С уважением, Константин Савенков.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking