FI:IA159 Formal Verification Methods - Informace o předmětu
IA159 Formal Verification Methods
Fakulta informatikyjaro 2014
- Rozsah
- 2/0. 2 kr. (plus ukončení). Ukončení: zk.
- Vyučující
- prof. 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 - Rozvrh
- Čt 14:00–15:50 B411
- 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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- Informační systémy (program FI, N-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- Počítačové systémy (program FI, N-IN)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- Služby - výzkum, řízení a inovace (angl.) (program FI, N-AP)
- Služby - výzkum, řízení a inovace (program FI, N-AP)
- Sociální informatika (program FI, B-AP)
- Teoretická informatika (program FI, N-IN)
- Učitelství výpočetní techniky pro střední školy (program FI, N-SS) (2)
- Umělá inteligence a zpracování přirozeného jazyka (program FI, N-IN)
- Zpracování obrazu (program FI, N-AP)
- Cíle předmětu
- At the end of this course, students should be able to: understand and explain principles, advandtages, and disadvantages of basic formal verification methods, namely model checking methods, symbolic execution, abstract interpretation, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems; - Osnova
- Overview of formal verification methods.
- 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.
- Bounded model checking.
- Symbolic execution.
- Static analysis, abstract interpretation.
- Verification tools.
- Literatura
- 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ě.
- Statistika zápisu (jaro 2014, nejnovější)
- Permalink: https://is.muni.cz/predmet/fi/jaro2014/IA159