Практика

Практическое задание

Задание состоит из двух этапов: формализация требований на ACSL и дедуктивная верификация одной из реализаций при помощи инструментов Frama-C + Jessie. Реализация выдается только после сдачи спецификации. Вопросы по заданию можно задавать в перерывах между занятиями или в ИСП РАН. Текст задания был вычитан, однако в нем могут остаться пропуски или нечетко сформулированные предложения. Исправления и уточнения будут помечаться в тексте задания.

<перейти к тексту задания>

Задания для практических аудиторных занятий

Задача 1. Треугольник.

Задача 2. Арифметическая последовательность.

Задача 3. Спецификация и верификация компонентов ядра JOS.