Рубрика: Новости

В весеннем семестре 2016/2017 учебного года занятия проходят с 14:35 до 17:55 в аудитории 505 каждый четверг.

Инструменты обновились сегодня. Настоятельно рекомендуется обновить их перед использованием. Для этого используйте команды opam update и opam upgrade.

10 июня в 10:00 состоится вторая контрольная работа по блоку спецификации для пропустивших её 28 апреля. Аудитория проведения станет известна в день проведения, узнавать в 718. Время работы 30 мин.

Экзамен обеих групп состоится 16 июня. Экзамен письменный, проводится с 10:00, длительность ориентировочно три часа. Экзамен проверяется в тот же день, показ работ после проверки, ближе к вечеру.

UPD: После начала экзамена (непосредственно после раздачи заданий) можно проставить автоматы.

Для получения верификационной части практического задания (после успешного выполнения спецификационной части) необходимо добавить вашу спецификацию к файлу map.h и прислать его. К функциям, не присутствующим в вашем варианте, не стоит добавлять никаких спецификационных комментариев.

Обратите внимание, что файл map.h со спецификацией нельзя менять во время выполнения верификационной части. Также, в выданных вам *.c-файлах все изменения должны составлять добавление спецификационных комментариев в отдельных строках этого файла. Остальные изменения файлов должны быть предварительно согласованы.

В реализации могут быть ошибки. При обнаружении ошибок, необходимо предложить исправление, согласовать его и только после этого продолжать верификацию.

Ближайшее занятие (19 мая) переносится из аудитории 609 в другую из-за проходящего госэкзамена. В какую именно должно быть написано на самой аудитории. Если ничего написано не будет, приходите в аудиторию 718.

На занятии 28 апреля будет проведена контрольная работа по блоку спецификации.

Напоминаю, что 14 апреля на лекции будет практическое занятие по пользованию связкой инструментов frama-c — jessie2 — why3. Постарайтесь, чтобы у всех были ноутбуки. Максимально желательно, чтобы вы попробовали установить связку инструментов. Инструкция по установке.

Напоминаю, что на семинаре 10 марта состоится контрольная работа по методам Флойда.

В весеннем семестре 2015/2016 года на факультете ВМК МГУ имени М.В. Ломоносова начинается ежегодное чтение курсов по формальной спецификации программ и дедуктивной верификации программ для магистров 1 года.