IA169 System Verification and Assurance

Fakulta informatiky
jaro 2016
Rozsah
2/2/2. 6 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k, z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
doc. RNDr. Vojtěch Řehák, Ph.D. (přednášející)
prof. RNDr. Václav Matyáš, M.Sc., Ph.D. (přednášející)
Dr. rer. nat. Achim Blumensath (cvičící)
Garance
prof. RNDr. Václav Matyáš, M.Sc., Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Út 12:00–13:50 A218
  • Rozvrh seminárních/paralelních skupin:
IA169/01: Út 10:00–11:50 A219, V. Řehák
IA169/02: Pá 10:00–11:50 A219, A. Blumensath
Předpoklady
(! IV113 Úvod do validace a verifikace ) && (!NOW( IV113 Úvod do validace a verifikace ))
User-level familiarity with Unix/Linux operating system. Basics of C programming. Basic astract math reasoning.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 32 stud.
Momentální stav registrace a zápisu: zapsáno: 0/32, pouze zareg.: 0/32, pouze zareg. s předností (mateřské obory): 0/32
Mateřské obory/plány
Cíle předmětu
The student will understand the necessary theoretic background as well as acquire hands-on experience with relevant tools for bug finding and formal verification techniques. With the help of a tutor students will get acquainted with a number of concrete software verification tools for analysis of concurrent systems, real-time systems, hybrid systems, cryptographic systems and systems with probabilities.
Osnova
  • This course will provide the necessary theoretic background as well as hands-on experience with relevant tools for bug finding and formal verification techniques. An introductory insight into security standards like Common Criteria for Information Technology Security Evaluation and FIPS 140 shall be provided first, together with a discussion of security threat models. Following this, the core topics of this course will include testing, simulations, advance testing and symbolic execution, abstract interpretation, static analysis, theorem proving, automated formal verification as well as an introduction to model-based verification. With the help of a tutor students will get acquainted with a number of concrete software verification tools for analysis of concurrent systems, real-time systems, hybrid systems, cryptographic systems and systems with probabilities.
Výukové metody
lectures, seminars/labs, homework assignments, readings
Metody hodnocení
Final (written) exam: 70%. Assignments: 30%.
Marking scheme: A for 90% or higher, then B for 80% or higher, then C for 70% or higher, then D for 60% or higher, then E for 50% or higher, then F(ail) for less than 50%.
Colloquy or credit – at least 44%.
Vyučovací jazyk
Angličtina
Navazující předměty
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2017, jaro 2018, jaro 2019, podzim 2019, podzim 2020, podzim 2021, podzim 2022, jaro 2024.