FI:IA159 Formal Verification Methods - Informace o předmětu

IA159 Formal Verification Methods

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 12:00–13:50 B410

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, advantages, 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.
• Abstraction.
• Counter-example guided abstraction refinement.
• Bounded model checking.
• 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

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 2015, nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/jaro2015/IA159