Joint Department with the RAS Institute for System Programming

Целями освоения программы «Верификация ПО» являются подготовка студентов к теоретическому и практическому применению методов анализа программного обеспечения (ПО); получение знаний в области статического анализа ПО, моделей кода, систем типов и их применения в анализе ПО, а также освоение инструментов анализа ПО. В рамках дисциплины изучаются такие разделы, как "Основы статического анализа программ", "Расширенные вопросы статического анализа программ".

Цель освоения дисциплины

подготовка студентов к теоретическому и практическому применению методов анализа программного обеспечения (ПО)
получение знаний в области статического анализа ПО, моделей кода, систем типов и их применения в анализе ПО
освоение инструментов анализа ПО

Планируемые результаты обучения

Демонстрирует знание метода ограниченной проверки моделей, интерпретирует контрпримеры SMT-решателя
Демонстрирует понимание направленного и ненаправленного анализа указателей
Знает понятие графа потока управления и моделей на его основе, понятие частично упорядоченного множества, теорему о наименьшей неподвижной точке
Знает понятие межпроцедурности в анализе ПО, применяет метод контекстной чувствительности на основе входных данных, знает понятие аппроксимации функции в программе
Знает понятие чувствительности к пути исполнения, умеет применять интервальный анализ и знает проблемы, связанные с ним, знает метод уточнения абстракции на основе контрпримеров
Знает понятия анализа и верификации ПО, основные подходы к статистическому анализу ПО, понятие абстрактного синтаксического дерева
Знает связь классических систем типов и анализа ПО, понятие анализа на основе ограничений, способы решения задачи присвоения типов, алгоритмы решения задачи унификации
Умеет анализировать указатели, динамическое выделение памяти и нулевые указатели
Умеет применять на практике потокочувствительный анализ
Умеет решать проблемы реализации анализов на основе бесконечных решеток, применяет методы объединения widening и narrowing

Содержание учебной дисциплины

Основы статического анализа программ
Расширенные вопросы статического анализа программ

Элементы контроля

Домашняя работа 1 (ДР1)
Домашняя работа 2 (ДР2)
Контрольная работа (КР)
Экзамен (Э)
Экзамен проводится дистанционно через Zoom. Технические требования: web-камера, микрофон, наушники / колонки, Zoom.
Домашняя работа 1 (ДР1)
Домашняя работа 2 (ДР2)
Контрольная работа (КР)
Экзамен (Э)
Экзамен проводится дистанционно через Zoom. Технические требования: web-камера, микрофон, наушники / колонки, Zoom.

Промежуточная аттестация

2022/2023 учебный год 2 модуль
В рамках курса студентам предлагается выполнить одну контрольную работу (оценка — Окр) и два домашних задания (оценки — Одом1 и Одом2). Текущая оценка (Отек) рассчитывается как сред-нее арифметическое оценок Окр, Одом1 и Одом2: Отек = 1/3 *·(Окр + Одом1 + Одом2). Накопленная оценка рассчитывается следующим образом: Онакопл = 0,6 * Отек + 0,4 * Осам. В диплом выставляет результирующая оценка по учебной дисциплине, которая формируется по следующей формуле: Орезульт = 0,6 * Онакопл + 0,4 * Оэкзамен, где Оэкзамен — оценка за устный экзамен. Округление при вычислении результирующей оценки осуществляется в пользу студента.

Contacts

Software Verification

Instructor

Программа дисциплины

Аннотация

Цель освоения дисциплины

Планируемые результаты обучения

Содержание учебной дисциплины

Элементы контроля

Промежуточная аттестация

Список литературы

Рекомендуемая основная литература

Рекомендуемая дополнительная литература