IA169 Model Checking

Fakulta informatiky
jaro 2024
Rozsah
2/1/0. 3 kr. (plus ukončení). Ukončení: zk.
Vyučováno prezenčně.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
RNDr. Martin Jonáš, Ph.D. (cvičící)
Garance
prof. RNDr. Jan Strejček, Ph.D.
Katedra teorie programování - Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování - Fakulta informatiky
Předpoklady
User-level familiarity with Unix/Linux operating system. Basic programming skills (Python). Some degree of abstract 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.: 23/130, pouze zareg. s předností (mateřské obory): 20/130
Mateřské obory/plány
předmět má 33 mateřských oborů, zobrazit
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. 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. The core topics of this course will include testing, symbolic execution, abstract interpretation, static analysis, theorem proving, automated formal verification as well as an introduction to model-based verification. 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. An introductory insight into security standards like Common Criteria for Information Technology Security Evaluation and FIPS 140 shall be provided as well.
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, 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
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích jaro 2016, jaro 2017, jaro 2018, jaro 2019, podzim 2019, podzim 2020, podzim 2021, podzim 2022.
  • Statistika zápisu (nejnovější)
  • Permalink: https://is.muni.cz/predmet/fi/jaro2024/IA169