Содиректор летней школы Microsoft Research Тони Хоар – один из основоположников формальной верификации

Лето – не только отдых, но и традиционно горячая трудовая пора у музыкантов, которые разъезжаются по всему миру на многочисленные фестивали. Не дают себе отдохнуть и молодые представители академического сообщества – своего рода фестивалями науки можно назвать летние школы по различным перспективным областям, традиция которых хорошо развита в Западной Европе, Америке и постепенно прививается и в России. В середине июля 2011 года прошла школа по программной инженерии и верификации, организованная исследовательским подразделением Microsoft Research и отделением программной инженерии Научно-исследовательского университета – Высшей школы экономики.

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

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

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

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