Летняя школа верификации

КЛЮЧЕВЫМ ЛЕКТОРОМ школы стал Тони Хоар – один из основоположников формальной верификации, работающий сейчас в отделении Microsoft Research в Кембридже Фото: Microsoft Research

В Москве прошла летняя школа по программной инженерии и верификации, организованная исследовательским подразделением Microsoft Research и отделением программной инженерии Научно-исследовательского университета — Высшей школы экономики.

Как пояснил содиректор школы Бен Лившиц из Microsoft Research, на подобные мероприятия корпорация собирает представителей академического сообщества и софтверной индустрии со всего мира, которые известны своими достижениями в области, выбранной в качестве темы школы. Это позволяет раскрыть тему максимально широко и дает студентам возможность пообщаться с разными специалистами, оценить различные стили и методы подачи материала.

Верификация представляет собой одну из самых сложных тем в области разработки ПО и призвана формальными математическими методами доказать корректность программы на основе анализа ее исходного кода. Ключевым лектором школы в Москве стал Тони Хоар — один из основоположников формальной верификации, лауреат премии Тьюринга, работающий сейчас в отделении Microsoft Research в Кембридже. В своем цикле лекций Хоар рассказал студентам о разработанных им алгебраических основах верификации. То, как эта теория может быть реализована в программном инструментарии для определения корректности кода, продемонстрировал Стефан Тобис, специалист Европейского центра инноваций Microsoft. Он представил систему верификации с открытым кодом VCC на примере верификации программ на языке Си. Эта система применялась в Microsoft, в частности для верификации исходного кода системы виртуализации Hyper-V.

Одной из целей московской школы было предоставить российским студентам и молодым ученым шанс почувствовать себя частью международного научного сообщества, изолированность от которого по-прежнему ощущается. Поэтому в качестве лекторов в школе приняли участие специалисты в области верификации и анализа программ из различных университетов и научных школ, в том числе Университета Лугано (Швейцария), Афинского университета, МГУ им. М.В. Ломоносова, Института системного программирования РАН, а также компаний Intel, Google и «Лаборатория Касперского». Некоторые из них читали не курсы, рассчитанные на весь срок школы, а отдельные лекции, открытые для свободного посещения. Среди таких «гостевых» лекторов был, например, Бертран Мейер — один из авторитетов в области программной инженерии, профессор Высшей политехнической школы в Цюрихе. Мейер рассказал об открытой среде верификации программ на разработанном им языке Eiffel.

Чтобы попасть на занятия школы, кандидаты должны были представить отборочному комитету результаты своих проектов или научные публикации, потому неудивительно, что большинство слушателей составили старшекурсники и аспиранты. Из почти 200 заявок, присланных молодыми людьми из 12 стран, было выбрано 70 человек. Отличительной особенностью школы стало то, что ее занятия не ограничивались лекциями — прийти и послушать интересных лекторов, может быть, выполнить их домашние задания, конечно, хорошо, но все-таки недостаточно. Задача школы — предоставить участникам возможность попробовать реализовать на практике то, о чем им рассказывают, поэтому студенты разбивались на небольшие команды по четыре-шесть человек для работы над проектами в тесном и свободном общении с лекторами, которые выступали в роли кураторов.