Этим летом с 17 по 27 июля в Москве приходила летняя школа Летняя школа по Программной Инженерии и Верификации, организованная совместно Microsoft Research, Высшей школой экономики, ИСП РАН. Я был ее участником(возможно самым молодым или одним из самых молодых) и очень хочу поделиться своими впечатлениями. Я не являюсь сотрудником Microsoft, просто публикую свое личное мнение и впечатление. Мне эта школа очень понравилась

Первым делом хочу сказать огромное спасибо организаторам и докладчикам, за очень интересное мероприятие. Краткое расписание лекций можно посмотреть тут а аннотацию к курсам тут. Все докладчики отжигали, особенно те, кто из Microsoft Research.

Общие вопросы Занятия проходили в офисе Microsoft в крылатском, а проживания для тех кто не из Москвы было в общежитии НИЯ-ВШЭ в Одинцово. Всего в школе участвовали около 70 человек из них 44 с РФ, остальные с Украины, Турции, Германии, Норвегии, Ирана. Большая часть аспиранты(плюс мое личное наблюдение, что почти у всех кольца на пальце=> явно не 15 лет детишкам) По поводу проживания у иностранцев были притензии, но отключение воды- это форсажор, от которого не страхует ни что! Питание было на убой просто и вкусно.

Теперь перехожу к делу Суть школы была в том, чтобы передать молодым участником опыт, который имели докладчики, навести контакты между участниками и просто рассказать, про технологии Microsoft и не Microsoft связанные с верификации программ, кода.

Первым докладчиком был Tony Hoare. Думаю, его представлять не надо. Великий человек, но тк я не математик, то мне его лекции были ой как тяжелы! О нем больше всего меня удивило, что он первую научную работу написал на русском языке, когда был на стажировке у Колмагорова.

Вторым докладчиком был Stephan Tobies, который нам рассказывал про VCC Человек, который занимался верификацией коды Hyper-v. Уже одно это вызывает уважение. Он был человеком, который рассказывал очень много интересного о том, как они верифицировали гипервизор. 100к строк кода, и 300к строк аннотаций к нему- вызвало уважение!

Следующим мне запомнился Andreys Sabelfeld. Суть его доклада была в том, что нужно защищать данные в программе. Условно- добавить новый атрибут к типу, который говорит защищенный он или нет, если защищенный, то работать он может тольк с доверенными функциями и переменными, чтобы исключить разглашение этих данных. На пример номер банковского счета, не мог быть скопирован и передан во вне. Конечно, можно подменить среду исполнения и отладчиком подключиться, но как известно на каждую защиту, можно найти средство обхода. Ах да, этот докладчик тоже знал русский, ибо сам вроде родился в Новосибирске.

Удивил нас и Yannis Smaragdakis... Рассказывать на школе Microsoft про анализ указателей на java- это круто. Если честно это наверное самая практическая часть была для меня, тк я от написания программ на С я очень далеко. Понятно, что в C# почти тоже самое с указателями, что и в Java, но сам факт, что MS может позволить себе так пойти против догм- это внушает уважение, что там были не зомби с промытыми мозгами.

На самом деле наверное обо всех докладчиках стоит рассказать, но думаю что сразу станет не интересно. Докладчики из Касперского(о чем могут говорить в касперском... о вирусах конечно), Intel(аппаратная верификация), ИСП РАН, университетов Европы- каждый заслуживает отдельной статьи, но в виду наличия работы пожалуй воздержусь от рассказа.

В конце школы, 2 последних дня был проект. Надо было собрать команду из 6 человек(2 иностранца. Украинцы за иностранцев тоже считались, хотя идея была, чтобы на английском работали все). Большая часть взялась поверифицировать что-то на vcc, на pex, кто-то решил что-то подаказывать в области алгебры. Команды были в реальности от 1 человека, до8 вроде. Я решил немного по обфусцировать веб данные, чтобы их было тяжело парсить, но визуальное представление было идентичным, чтобы человеку было все так же удобно.

Из культурных event был поход в планетарий Московский(от себя скажу, что обалденно романтичное место, чтобы девушку вести.) Потом ребята ходили на Красную площадь, было 2 мероприятия, когда все собирались в кофе социолизироваться(говорят коктейли были вкусные, но я не пробовал). Общение с умными, талантливыми людьми всегда доставляет удовольствие. Докладчики все были очень открыты, обсуждение докладов в столовой шло на ура! Честно говоря мне кажется, что эти обсуждения были едва ли не важнее самих лекций, тк в столовой можно было спросить и узнать все, даже не относящееся к лекции.

В последний день к нам привели Сошникова Дмитрия(академический евангелист) и человека отвечающего за Microsoft Research в России. Как вы догадываетесь главный вопрос был- как к вам попасть! Ответ- работайте, пишите письма тем чьи проекты вам нравятся и у вас есть опыт, который вы готовы внести. В общем как всегда

В общем было очень интересно, спасибо докладчикам и организаторам! Ждем в следующем году таких мероприятий от Microsoft!

Ссылки на страницы мероприятия: http://vk.com/sssev2011