Операционные системы UNIX и анализ правильности параллельных программ

Д. М. Лебединский
магистратура, семестр 3

Дисциплина имеет целью ознакомление студентов с моделями и методами рассуждений о правильности работы программ, в том числе параллельных. В ней освещаются следующие темы: способы доказательства правильности последовательных и параллельных программ, основанные на разметке блок-схем или логике программирования; система SPIN, предназначенная для автоматической проверки правильнсти параллельных программ и протоколов методом исчерпывающего перебора состояний модели, и язык Promela, на котором пишутся такие модели; некоторые программные средства для автоматического поиска в программах гонок за данными и взаимоблокировок. Вид занятий — лекции. Изучив данную дисциплину, студент должен уметь математически доказывать правильность несложных программ, а также автоматически проверять правильность более сложных программ, используя упомянутые инструменты.