IA159 Formal Verification Methods

Fakulta informatiky
jaro 2018
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
doc. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování - Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování - Fakulta informatiky
Předpoklady
IV113 Úvod do validace a verifikace || IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Výstupy z učení
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including translation of LTL to Büchi automata and partial order reduction.
  • Abstraction.
  • Counterexample-guided abstraction refinement.
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001. xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999. xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
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 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017.

Nahoru | Aktuální datum a čas: 19. 11. 2017 07:44, 46. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému