Навчання > Надійність програмних систем (122 – кн)

Надійність програмних систем (122 – кн)

Тип: На вибір ВУЗу

Кафедра: інформаційних систем

Навчальний план

СеместрКредитиЗвітність
96Залік

Лекції

СеместрК-сть годинЛекторГрупа(и)
932професор, ст. наук. співробітник Жолткевич Г. М.ПМі-51м

Лабораторні

СеместрК-сть годинГрупаВикладач(і)
932ПМі-51мпрофесор, ст. наук. співробітник Жолткевич Г. М.

Опис курсу

Навчальну дисципліну розроблено так, щоб забезпечити розуміння студентами концепції надійності технічних систем, її особливості для програмних систем, а також ознайомити студентів з сучасною технологією забезпечення розробки надійного програмного забезпечен­ня ‒ сертифікованим програмування, спираючись на можливості Rocq Prover (раніше The Coq Proof Assistant) та сформувати загальні навички її використання.

Курс представляє собою приклади застосування технології сертифікованого програмування для низки простих але типових задач програмування з поясненням загальних концепцій на цих прикладах. Кожна лекція передбачає обговорення на лабораторному занятті з широким залученням студентів до такого обговорення.

Рекомендована література

Основна література

  1. Chlipala, Adam. Certified Programming with Dependent Types, MIT Press, 2019.
  2. Bertot, Yves and Casteran, Pierre. Interactive Theorem Proving and Program Development. Coq’ Art: The Calculus of Inductive Constructions, Springer, 2004.
  3. Chlipala, Adam. Formal Reasoning About Programs, MIT Press, 2023.
  4. Paulin-Mohring, Christine. Introduction to the Coq proof-assistant for practical software verification, Lecture Notes in Computer Science, vol 7682. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35746-6_3.
  5. The Rocq Prover Development Team. The Rocq Prover Reference Manual. 2026. https://rocq-prover.org/doc/V9.2.0/refman/index.html#
  6. The Rocq Prover Development Team. The Rocq Prover Standard Library. 2026. https://rocq-prover.org/doc/V9.1.0/refman-stdlib/index.html

Додаткова література

  1. Software Foundations Volume 1. Logical Foundation. https://softwarefoundations.cis.upenn.edu/current/lf-current/index.html
  2. Software Foundations Volume 2. Programming Language Foundations. https://softwarefoundations.cis.upenn.edu/current/plf-current/index.html
  3. Software Foundations Volume 3. Verified Functional Algorithms. https://softwarefoundations.cis.upenn.edu/current/vfa-current/index.html
  4. Software Foundations Volume 5. Verifiable C. https://softwarefoundations.cis.upenn.edu/current/vc-current/index.html

Силабус: Надійність програмних систем (2022)

Завантажити силабус

Силабус: Надійність програмних систем (2023)

Завантажити силабус

Силабус: Надійність програмних систем (2024)

Завантажити силабус