Conferences system

Однодневный международный научный семинар пройдёт в субботу 13 июля 2013 г. в Санкт-Петербурге при 25-ой Международной конференции по автоматизированной верификации (25th International Conference on Computer Aided Verification, http://cav2013.forsyte.at)

Мотивация
Минуло уже 45 года с момента публикации Робертом В. Флойдом статьи Assigning Meanings to Programs, в которой была сделана первая (и удачная) попытка разработать математически-точный метод описания формальной семантики (смысла) программ. Уже прошло 15 лет после публикации Дэвидом А. Шмидтом призыва к академической общественности сделать формальную семантики программ понятной и доступной широкому кругу инженеров-программистов. Однако совсем недавно Дэвид Л. Парнас выступил с призывом  Really Rethinking “Formal Methods” из-за того, что формальными методами по-прежнему больше занимаются теоретики, чем разработчики программного обеспечения.

На наш взгляд польза от формальных методов не исчерпывается их использованием в разработке и производстве программного обеспечения; почти по Ломоносову: формальные методы в программировании уж затем учить надо, что они ум в порядок приводят. Разумеется, математика имеет множество практических приложений, и формальные методы тоже должны найти своё применение в практике программной инженерии, но роль формальных методов и математики для образования будущих программистов тоже имеет немалое значение. 

Однако, тут мы наталкиваемся на хроническую аллергию программистов (студентов и инженеров) к формальным методам: они их находят слишком «рафинированными» в теории и неэффективными на практике. На наш взгляд основа этой устойчивой аллергии – отсутствие элементарных (как в начальной школе) курсов по формальным методам. Общепризнано, что обучение арифметики нельзя начинать с аксиоматики Пеано, но сначала  решают задачи о числе слив, яблок, карандашей и т.д. Например, никто не предлагает сразу учить манипуляциям с доказательствами и не предлагает учащимся показать, что  в арифметике Пеано доказуемо (y≤z → ((x+y) – z) = (x + (y – z))) для всех x, y и z, но для начала учит как решать задачки вроде следующей: Пете дали 5 яблок, а он отдал 2 яблока Ване; сколько яблок осталось у Пети? (Если Вы думаете, что у Пети осталось 3 яблока, то ошибаетесь: у него осталось как минимум 3 яблока.)

По нашему мнению, аллергия на формальные методы во многом объясняется тем, что эксперты не заботятся о начальном уровне обучения формальным методам. Курсы по формальным методам обычно начинаются с введения понятий абстрактная машина состояний, преобразователь предикатов, логический вывод, операционная семантика, денотационная семантика, аксиоматическая семантика и – никаких элементарных и научно-популярных пояснений.

Тематика семинара
1. Искусство применения формальных методов при разработке программ,
2. опыт популяризации формальных методов,
3. использование формальных методов для решения головоломок,
4. нестандартные применения формальных методов,
5. и все остальное, что раскрывает красоту формальных методов.

Приглашённые пленарные докладчики
1. Юрий Глебович Карпов (Санкт-Петербургский государственный политехнический университет)
2. John Rushby (SRI International, California, USA)

Программный комитет
• Paul Curzon (Queen Mary, University of London)
• Виктор Вячеславович Кулямин (Институт системного программирования РАН, Моска)
• Dominique Mery (LORIA & Université de Lorraine, France)
• Николай Николаевич Непейвода (Институт программных систем РАН, Переславль-Залеский)
• Николай Вячеславович Шилов (организатор FWFM, Институт систем информатики СО РАН, Новосибирск)
• Ростислав Эдуардович Яворский («Сколков»)

Шилов Николай Вячеславович

Институт систем информатики СО РАН, пр. Лаврентьева, д.6, г. Новосибирск, 630090

тел. (383) 330 62 53

факс(383( 332 34 94