IA159 Formal Verification Methods

Fakulta informatiky
jaro 2013
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
doc. Mgr. Jan Obdržálek, PhD. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. Mgr. Jan Obdržálek, PhD.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 12:00–13:50 G123
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 Modální a temporální logiky procesů and IV113 Úvod do validace a verifikace before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should be able to: understand and explain principles of basic formal verification methods, namely model checking methods, reachability analysis, symbolic execution, abstract interpretations, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • Software testing.
  • Deductive verification methods (theorem proving).
  • LTL model checking of finite and infinite-state systems.
  • State explosion problem, partial order reduction, abstraction.
  • Counter-example guided abstraction refinement.
  • Symbolic execution.
  • Static analysis, abstract interpretation.
  • Verification tools.
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
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
Výukové metody
lectures
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ě.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.