Верифікація мікропроцесорів
Робоча програма навчальної дисципліни (відповідно до вимог МОН України).
Документ містить мету, результати навчання, структуру змісту, систему оцінювання та літературу.
Код курсу: КА-121-03
Кафедра: Кафедра мовного забезпечення
Кількість кредитів ECTS: 6 (180 годин)
Рівень: Бакалавр / Магістр
Мета та завдання
Формування глибоких знань і практичних навичок у галузі «Верифікація мікропроцесорів». Курс інтегрує класичні результати з сучасними формальними методами (теорія типів, категорійна логіка, механічна верифікація), відповідно до профілю Кафедра мовного забезпечення.
Результати навчання
- Володіти основними поняттями та конструкціями курсу «Верифікація мікропроцесорів».
- Застосовувати теоретичні результати до розв’язання задач.
- Формалізувати ключові твердження в системах доведення теорем (за можливості).
- Демонструвати навички самостійного дослідження та академічної доброчесності.
Структура курсу (модулі)
- Теоретичні основи
- Алгоритми та реалізації
- Інструменти верифікації
- Практичні кейси
- Формальні методи
Система оцінювання (100 балів)
- Поточний контроль (практичні, домашні, лабораторні, формалізація): 40 балів
- Модульні контрольні роботи (2): 20 балів
- Підсумковий іспит / захист проєкту: 40 балів
Шкала: 90–100 — відмінно; 75–89 — добре; 60–74 — задовільно; <60 — незадовільно.
Рекомендована література
- Основні монографії та підручники з теми (рекомендовані кафедрою).
- Статті та матеріали з формальної математики (HoTT, теорія категорій).
- Внутрішні конспекти та формалізації Інституту Формальної Математики / Groupoid Infinity.