• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Книга
ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction

Под науч. редакцией: Vitaly Semenov, R. J. Scherer.

CRC Press, 2021.

Статья
Equivalence checking and intersection of deterministic timed finite state machines

Bresolin D., El-Fakih K., Villa T. et al.

Formal Methods in System Design. 2022.

Глава в книге
City and building information modelling using IFC standard

Shutkin V., Morozkin N., Zolotov V. et al.

In bk.: ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction. CRC Press, 2021. P. 406-413.

Препринт
Preventive Model-based Verification and Repairing for SDN Requests

Burdonov I., Kossachev A., Nina Yevtushenko et al.

arxiv.org. Computer Science. Cornell University, 2020

Верификация программного обеспечения

2022/2023
Учебный год
RUS
Обучение ведется на русском языке
6
Кредиты

Преподаватель

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

Аннотация

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

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

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

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

  • Демонстрирует знание метода ограниченной проверки моделей, интерпретирует контрпримеры 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 * Оэкзамен, где Оэкзамен — оценка за устный экзамен. Округление при вычислении результирующей оценки осуществляется в пользу студента.
Список литературы

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

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

  • Mukherjee, S., & Blasband, D. (2016). Source Code Analytics With Roslyn and JavaScript Data Visualization. [Berkeley, CA]: Apress. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=1450659

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

  • Forest, E. (2016). From Tracking Code to Analysis : Generalised Courant-Snyder Theory for Any Accelerator Model. Japan: Springer. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=1178523
  • Hyde, R. (2004). Write Great Code, Volume 1 : Understanding the Machine. San Francisco, CA: No Starch Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=440094
  • van der Linden, M. A. (2007). Testing Code Security. Boca Raton, FL: Auerbach Publications. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=928213