FI:IA169 System Verif. and Assurance - Informace o předmětu
IA169 System Verification and Assurance
Fakulta informatikypodzim 2020
- Rozsah
- 2/0/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
- 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í)
RNDr. Marek Chalupa, Ph.D. (cvičící) - Garance
- prof. RNDr. Jiří Barnat, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- St 16:00–17:50 A217
- Rozvrh seminárních/paralelních skupin:
IA169/02: Po 10:00–11:50 A219, M. Chalupa, V. Řehák - 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 130 stud.
Momentální stav registrace a zápisu: zapsáno: 0/130, pouze zareg.: 0/130, pouze zareg. s předností (mateřské obory): 0/130 - Mateřské obory/plány
- Analýza a zpracování obrazu (program FI, N-VIZ)
- Bezpečnost informačních technologií (angl.) (program FI, N-IN)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika a systémová biologie (program FI, N-UIZD)
- Computer Games Development (program FI, N-VIZ_A)
- Computer Graphics and Visualisation (program FI, N-VIZ_A)
- Computer Networks and Communications (program FI, N-PSKB_A)
- Cybersecurity Management (program FI, N-RSSS_A)
- Formální analýza počítačových systémů (program FI, N-TEI)
- Grafický design (program FI, N-VIZ)
- Graphic Design (program FI, N-VIZ_A)
- Hardware Systems (program FI, N-PSKB_A)
- Hardwarové systémy (program FI, N-PSKB)
- Image Processing and Analysis (program FI, N-VIZ_A)
- Informační bezpečnost (program FI, N-PSKB)
- Information Security (program FI, N-PSKB_A)
- Kvantové a jiné neklasické výpočetní modely (program FI, N-TEI)
- Paralelní a distribuované systémy (program FI, B-IN)
- Počítačová grafika a vizualizace (program FI, N-VIZ)
- Počítačové sítě a komunikace (program FI, N-PSKB)
- Principy programovacích jazyků (program FI, N-TEI)
- Řízení kyberbezpečnosti (program FI, N-RSSS)
- Řízení vývoje služeb (program FI, N-RSSS)
- Řízení vývoje softwarových systémů (program FI, N-RSSS)
- Services Development Management (program FI, N-RSSS_A)
- Software Systems Development Management (program FI, N-RSSS_A)
- Software Systems (program FI, N-PSKB_A)
- Softwarové systémy (program FI, N-PSKB)
- Strojové učení a umělá inteligence (program FI, N-UIZD)
- Vývoj počítačových her (program FI, N-VIZ)
- Zpracování a analýza rozsáhlých dat (program FI, N-UIZD)
- Zpracování přirozeného jazyka (program FI, N-UIZD)
- 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.
- Výstupy z učení
- Students will:
be aware of fundaments of black-box testing;
understand priciples of deductive verification;
understand the theory and application of model checking;
have hand-on experince with a couple of verification tools. - 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.
- Literatura
- GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
- Výukové metody
- lectures, seminars/labs, homework assignments, readings
- Metody hodnocení
- Final (written) exam: 50%. Assignments: 50%.
Marking scheme: A for 85% or higher, then B for 80% or higher, then C for 75% or higher, then D for 70% or higher, then E for 65% or higher, then F(ail) for less than 65%.
Colloquy or credit – at least 65%. - 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ě.
- Statistika zápisu (podzim 2020, nejnovější)
- Permalink: https://is.muni.cz/predmet/fi/podzim2020/IA169