Informace o předmětu

IA169 Model Checking

Rozsah

2/1/0. 3 kr. (plus ukončení). Ukončení: zk.

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

Rozvrh

Po 19. 2. až Čt 9. 5. Čt 16:00–17:50 A318

• Rozvrh seminárních/paralelních skupin:

IA169/01: Po 19. 2. až Čt 9. 5. každý sudý čtvrtek 18:00–19:50 A318, M. Jonáš

Předpoklady

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: 12/130, pouze zareg.: 0/130, pouze zareg. s předností (mateřské obory): 0/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 fundamental and currently used model checking algorithms and techniques (except those primarily designed for software). Further, the student will be able to read and write specifications in LTL and CTL, and use relevant formalisms like Büchi automata and binary decision diagrams.

Výstupy z učení

Students will:
understand traditional model checking algorithms (LTL and CTL model checking) and current approaches (bounded model checking, k-induction, CEGAR, property-driven reachability);
be able to read and write specifications in LTL and CTL;
be aware of potential applications and inherent limitations of model checking algorithms.

Osnova

• Overview of the model checking area.
• Kripke structure, labelled transition system, LTL, CTL, Büchi automata.
• Automata-based LTL model checking.
• CTL model checking.
• Bounded model checking and k-induction.
• Reachability in pushdown systems.
• Abstraction and CEGAR.
• Property directed reachability.

Literatura

• CLARKE, E. M., Orna GRUMBERG, Doron PELED, Daniel KROENING a Helmut VEITH. Model checking. Second edition. Cambridge, Massachusetts: MIT Press, 2018, xx, 402. ISBN 9780262038836. info
• Handbook of model checking. Edited by E. M. Clarke - T. A. Henzinger - Helmut Veith - Roderick Bloem. Cham: Springer International Publishing AG, 2018, xxiv, 1210. ISBN 9783319105741. info

Výukové metody

lectures, seminars

Metody hodnocení

oral exam

Vyučovací jazyk

Angličtina

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 System Verification and Assurance

Rozsah

2/0/2. 4 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
doc. RNDr. Vojtěch Řehák, Ph.D. (cvičící)
Mgr. Pavol Žáčik (cvičící)
prof. RNDr. Václav Matyáš, M.Sc., Ph.D. (pomocník)

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

Předpoklady

(! IV113 Úvod do validace a verifikace ) && (!NOW( IV113 Úvod do validace a verifikace ))
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: 15/130, pouze zareg.: 0/130, pouze zareg. s předností (mateřské obory): 0/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

• IA159 Formal Methods for Software Analysis

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 System Verification and Assurance

Rozsah

2/0/2. 4 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
RNDr. Marek Chalupa, Ph.D. (cvičící)
doc. RNDr. Vojtěch Řehák, Ph.D. (cvičící)
prof. RNDr. Václav Matyáš, M.Sc., Ph.D. (pomocník)

Garance

prof. RNDr. Jiří Barnat, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

St 15. 9. až St 8. 12. St 16:00–17:50 D1

• Rozvrh seminárních/paralelních skupin:

IA169/Konzultace_k_DU: Po 13. 9. až Po 6. 12. Po 16:00–17:50 A219, J. Barnat, 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. 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: 1/130, pouze zareg.: 0/130, pouze zareg. s předností (mateřské obory): 0/130

Mateřské obory/plány

předmět má 32 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

• IA159 Formal Methods for Software Analysis

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 System Verification and Assurance

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/01: St 12:00–13:50 A219, M. Chalupa, V. Řehák
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

předmět má 32 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. 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

• IA159 Formal Methods for Software Analysis

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 System Verification and Assurance

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/01: St 12:00–13:50 A219, M. Chalupa, V. Řehák
IA169/02: Po 12:00–13: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 70 stud.
Momentální stav registrace a zápisu: zapsáno: 1/70, pouze zareg.: 0/70, pouze zareg. s předností (mateřské obory): 0/70

Mateřské obory/plány

předmět má 32 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. 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

• IA159 Formal Methods for Software Analysis

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 System Verification and Assurance

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í)
RNDr. Marek Chalupa, Ph.D. (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 19. 2. až Út 14. 5. Út 12:00–13:50 A319

• Rozvrh seminárních/paralelních skupin:

IA169/01: Čt 21. 2. až Čt 16. 5. Čt 12:00–13:50 A219, M. Chalupa, V. Řehák
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 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

• Bezpečnost informačních technologií (angl.) (program FI, N-IN)
• Bezpečnost informačních technologií (program FI, N-IN)

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

• IA159 Formal Methods for Software Analysis

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 System Verification and Assurance

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í)
RNDr. Marek Chalupa, Ph.D. (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 8:00–9:50 A219, M. Chalupa, V. Řehák
IA169/02: St 14:00–15: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 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

• Bezpečnost informačních technologií (angl.) (program FI, N-IN)
• Bezpečnost informačních technologií (program FI, N-IN)

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

• IA159 Formal Methods for Software Analysis

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 System Verification and Assurance

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í)
RNDr. Marek Chalupa, Ph.D. (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 B410

• Rozvrh seminárních/paralelních skupin:

IA169/01: Po 16:00–17:50 A219, V. Řehák
IA169/02: St 18:00–19:50 A219, M. Chalupa

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

• Bezpečnost informačních technologií (angl.) (program FI, N-IN)
• Bezpečnost informačních technologií (program FI, N-IN)

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

• IA159 Formal Methods for Software Analysis

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 System Verification and Assurance

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

• Bezpečnost informačních technologií (angl.) (program FI, N-IN)
• Bezpečnost informačních technologií (program FI, N-IN)

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

• IA159 Formal Methods for Software Analysis

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

IA169 Model Checking

Předmět se v období jaro 2025 nevypisuje.

Rozsah

2/1/0. 3 kr. (plus ukončení). Ukončení: zk.
Vyučováno kontaktně

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

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.: 2/130, pouze zareg. s předností (mateřské obory): 0/130

Mateřské obory/plány

předmět má 30 mateřských oborů, zobrazit

Cíle předmětu

The student will understand the fundamental and currently used model checking algorithms and techniques (except those primarily designed for software). Further, the student will be able to read and write specifications in LTL and CTL, and use relevant formalisms like Büchi automata and binary decision diagrams.

Výstupy z učení

Students will:
understand traditional model checking algorithms (LTL and CTL model checking) and current approaches (bounded model checking, k-induction, CEGAR, property-driven reachability);
be able to read and write specifications in LTL and CTL;
be aware of potential applications and inherent limitations of model checking algorithms.

Osnova

• Overview of the model checking area.
• Kripke structure, labelled transition system, LTL, CTL, Büchi automata.
• Automata-based LTL model checking.
• CTL model checking.
• Bounded model checking and k-induction.
• Reachability in pushdown systems.
• Abstraction and CEGAR.
• Property directed reachability.

Literatura

• CLARKE, E. M., Orna GRUMBERG, Doron PELED, Daniel KROENING a Helmut VEITH. Model checking. Second edition. Cambridge, Massachusetts: MIT Press, 2018, xx, 402. ISBN 9780262038836. info
• Handbook of model checking. Edited by E. M. Clarke - T. A. Henzinger - Helmut Veith - Roderick Bloem. Cham: Springer International Publishing AG, 2018, xxiv, 1210. ISBN 9783319105741. info

Výukové metody

lectures, seminars

Metody hodnocení

oral exam

Vyučovací jazyk

Angličtina

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.
Výuka probíhá každý týden.

IA169 System Verification and Assurance

Předmět se v období jaro 2015 nevypisuje.

Rozsah

2/2/2. 6 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
prof. RNDr. Václav Matyáš, M.Sc., Ph.D. (přednášejí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

Předpoklady

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 otevřen studentům libovolného oboru.
Předmět si smí zapsat nejvýše 30 stud.
Momentální stav registrace a zápisu: zapsáno: 0/30, pouze zareg.: 0/30, pouze zareg. s předností (mateřské obory): 0/30

Cíle předmětu

This course will provide the necessary theoretic background as well as 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

• IA159 Formal Methods for Software Analysis

• Statistika zápisu (nejnovější)