Уважаемые студенты 1-2 курса!
Многие из вас хотели бы выбрать в качестве основного
направления своей научной специализации такую область,
которая с одной стороны была бы связана с глубокой математикой,
и с другой стороны имела бы большую практическую актуальность.
Одной из таких областей является теория анализа корректности компьютерных программ.
Задача анализа корректности программы заключается в следующем.
Дан текст программы и спецификация этой программы
(т.е. описание того, что программа должна делать: например связь между
входными и выходными данными).
Требуется формально доказать, что программа удовлетворяет своей спецификации.
Например, анализируемая программа - это реализация некоторого
алгоритма сортировки, а спецификация - это формула в языке первого порядка
от двух переменных, пробегающих все массивы натуральных чисел,
которая истинна на паре массивов тогда и только тогда когда второй
массив - это отсортированный первый.
Программа может представлять собой также описание функционирования
некоторого вычислительного устройства (например, перемножителя чисел
с плавающей точкой).
Задачи анализа программ представляют исключительную актуальность:
в тех условиях когда программы управляют такими объектами как
самолеты, атомные электростанции, и т.д. от надежности этих программ
существенно зависит безопасность людей.
Известно, что многие катастрофы на технических объектах были вызваны
некачественным программным обеспечением.
Теория формального анализа программ находится в состоянии
исключительно бурного развития.
Математические задачи, возникающие при решении проблем
анализа программ, отличаются большой трудностью и требуют
для своего решения создания принципиально новых математических методов,
связанных с алгеброй, логикой, дискретной математикой, теорией вероятностей.
К сожалению, пока на мехмате нет ни одного семинара, посвященного
этому направлению.
Но принципиальных трудностей, препятствующих
созданию такого семинара уже в этом семестре, нет.
Он может быть организован уже в этом семестре, если
будет достаточное количество студентов мехмата,
желающих специализироваться в этом направлении.
Те из вас, кто заинтересован в специализации в этом направлении,
просьба писать мне по адресу mironov@unb.ca
Желаю успехов,
Андрей Миронов http://www.cs.unb.ca/profs/mironov
P.S. Более подробно узнать о некоторых подходах к анализу программ
можно из моей статьи по адресу
http://www.cs.unb.ca/profs/mironov/rus_ag.ps
