model-checking Апрель 2012

model-checking@asvk.cs.msu.ru

1 участники
6 обсуждения

Информация о конкурсе по анализу данных
by model checking course mailing list 28 Апр '12

28 Апр '12

Дорогие студенты, На лекции меня попросили продублировать в рассылку информацию о конкурсе. 26 апреля стартовал конкурс рекомендательных систем Million Song Dataset Challenge (http://www.kaggle.com/c/msdchallenge <http://www.kaggle.com/c/msdchallenge>)/. Организаторы - /CAL UCSD/,/LabROSA CU, The EchoNest, IMIRSEL и UIUC. Завершение -- через три месяца, 9 августа. В ходе конкурса нужно построить систему, которая по 100% истории прослушивания музыки для 1М пользователей и 50% истории для 100К пользователей сможет максимально точно достроить недостающие 50%. При этом можно пользоваться любыми другими данными (анализ аудио, метаданные, ноты, тексты песен итп) и подходами. Как такового приза у конкурса нет, но компания Zvooq (http://zvooq.ru <http://zvooq.ru/>) решила сделать его чуть более интересным для российских участников. Лучшая команда из России получит $5000 и возможность бесплатно отправить одного участника на конференцию ISMIR 2012 (http://ismir2012.ismir.net/). На конференции, например, можно с легкостью найти лабораторию для написания PhD. Постер с более детальной информацией -- в приложении. С уважением, Константин Савенков.

1 0

Model Checking Task 5
by model checking course mailing list 28 Апр '12

28 Апр '12

??? ?????? ? ??????? ??????? ????????? ? ??????????? ??? ??? ??????: 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 ????? ????? -- ?????? 14-18 ???. ?????-?????????-?????-?????-???????? ????? ? ???????? ??????, ??? ?? ????? ?????????? ?????? ?? ????????? ???? (?????????? ???? ?????? ?????). ? ?????????, ?????????? ????????.

1 0

Итоги приема 2-го задания
by model checking course mailing list 24 Апр '12

24 Апр '12

Дорогие студенты, Оценки внесены в таблицу. Проверяйте. Не прислали копии решений (баллы аннулированы): ГРИГОРЯН КАРЭН РОБИКОВИЧ ПУЗИКОВ БОРИС ЮРЬЕВИЧ СЕЛЕВЕНКО ВЛАДИМИР Если пришлете сегодня, то м.б. разаннулирую обратно. Со временем проверим: ЕРОФЕЕВ МИХАИЛ ВИКТОРОВИЧ МЕРКУЛОВ КИРИЛЛ ДМИТРИЕВИЧ СУДАРИКОВ ИГОРЬ ВАЛЕРЬЕВИЧ ЖУРАХОВСКИЙ ОЛЕГ АНДРЕЕВИЧ ТИПИСОВА АЛИСА ОЛЕГОВНА МАКСИМЕНКО НИКИТА АНДРЕЕВИЧ ВТОРОВ АЛЕКСАНДР АЛЕКСАНДРОВИЧ ПЕРЕХОДЬКО ЕВГЕНИЯ ЯКОВЛЕВНА СТЕПАНОВ ВИКТОР СЕРГЕЕВИЧ Не сдавали: 420: ПУТИЛИН АЛЕКСАНДР ВЛАДИМИРОВИЧ 421: БАТАНОВ ПАВЕЛ ГЕОРГИЕВИЧ ЗАЧЕСОВ АНТОН АЛЕКСАНДРОВИЧ 422: ГАЙДОВ ВИКТОР ВИКТОРОВИЧ СОРОКИН АЛЕКСАНДР ИГОРЕВИЧ 424: ЛОЗА ИЛЬЯ ОЛЕГОВИЧ МАРУЛИН ВЛАДИМИР ВЛАДИМИРОВИЧ ПОЯРКОВА ДАРЬЯ АЛЕКСАНДРОВНА Нетребко Станислав Алексеевич 427: ГОЛУШКО ПАВЕЛ АЛЕКСАНДРОВИЧ ДОЛОТКАЗИН ЮРИЙ ВЛАДИМИРОВИЧ КИРОВ ДМИТРИЙ НИКОЛАЕВИЧ МИХАЙЛОВ АЛЕКСАНДР НИКОЛАЕВИЧ СЕЛЕЗНЁВ ВЛАДИМИР ДМИТРИЕВИЧ С уважением, Константин Савенков

1 0

Занятия 28 апреля
by model checking course mailing list 24 Апр '12

24 Апр '12

Дорогие студенты, Напоминаю, что 28 апреля, как это не печально, занятия по расписанию понедельника, то есть будет и лекция, и практикум. С уважением, Константин Савенков.

1 0

Поправка
by model checking course mailing list 09 Апр '12

09 Апр '12

Дедлайн по 3-му заданию: неделя 16-20 апреля, финальный дедлайн по нему же - неделя 28.04-05.05 (либо дни, на которые перенесены занятия). С уважением, Константин Савенков.

1 0

Две новости
by model checking course mailing list 09 Апр '12

09 Апр '12

Дорогие студенты, Во-первых, следующая лекция будет 28 апреля, на которое (вроде бы) перенесен понедельник 30.04. Во-вторых, для нейтрализации ддос-атак на принимающих практикум, давайте сделаем так: дедлайн по третьему заданию -- неделя с 9 по 13 апреля, в соответствии с расписанием (для каждой группы -- в день семинара на этой неделе). Финальный дедлайн -- так же, но на неделе 23-27 апреля. С уважением, Константин Савенков.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Апрель 2012