Содержание спецкурса составляют классические методы верификации программ, которые базируются на подходах Флойда и Хоара. Вначале вводится логический язык спецификаций, на базе которого определяется понятие корректности программ. Подробно рассматривается метод аксиоматической семантики как для элементарных конструкций, циклов и процедур, так и для операторов над сложными структурами данных, такими как массивы, файлы, указатели. Рассматривается проблема автоматизации трудоемкого процесса верификации программ.

Основные принципы Открытых Связанных Данных за последние годы были приняты большим числом поставщиков данных, что привело к созданию глобального пространства данных, которое содержит многие миллиарды утверждений –Web of Data. Среди предприятий, использующих новые стандарты и активно участвующих в развитии этого направления находятся Google, Facebook, Microsoft, IBM и многие другие.

Цель курса - общее представление о функциональном программировании и сфере его применения, включая анализ основных понятий и принципов, связь функционального программирования с математическими основами на материале разных языков. В настоящее время очередной всплеск интереса к функциональному программированию связан с поиском методов параллельного программирования для суперкомпьютеров, графических процессоров и других мультипроцессорных конфигураций.