Специальный курс «Практическое введение в формальную верификацию в системе PVS» (Practicum on formal verification in PVS)

Лектор: Корныхин Евгений Валерьевич.
Продолжительность: 36 часов лекции.
Семестр: осенний.
Аудитория: для студентов бакалавриата (3-4 курс).
Форма отчётности: зачёт или экзамен в зависимости от учебного плана слушателя.
Лекции в 2025 г. читаются по вторникам в 8-45 в ауд. 507.

Аннотация

Спецкурс дает практические навыки по формальнойспецификации программных систем и их прототипов и их верификации при помощи инструмента PVS. Этот инструмент активно используется в NASA. Подобные инструменты используются в ИСП РАН, РуcБИТех (Astra Linux), Лаборатории Касперского и др..

Литература:
1. Prototype Verification System: https://pvs.csl.sri.com/
2. N. Shankar, S. Owre, J. M. Rushby, D. W. J. Stringer-Calvert. PVS System Guide, version 7.1, august 2020: https://pvs.csl.sri.com/doc/pvs-system-guide.pdf
3. N. Shankar, S. Owre, J. M. Rushby, D. W. J. Stringer-Calvert. PVS Language Reference, version 7.1, august 2020: https://pvs.csl.sri.com/doc/pvs-language-reference.pdf
4) N. Shankar, S. Owre, J. M. Rushby, D. W. J. Stringer-Calvert. PVS Prover Guide, version 7.1, august 2020: https://pvs.csl.sri.com/doc/pvs-prover-guide.pdf

Размещение на других ресурсах, а также коммерческое использование материалов, опубликованных в данном разделе, возможно только с разрешения авторов.

© Кафедра системного программирования ВМК МГУ.

Обновлено: 17.IX.2025