DFOME Formální metody v teorii i praxi

Fakulta informatiky
jaro 2014
Rozsah
3/0. 3 kr. Ukončení: z.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející)
prof. RNDr. Ivana Černá, CSc. (přednášející)
prof. RNDr. Petr Hliněný, Ph.D. (přednášející)
prof. RNDr. Mojmír Křetínský, CSc. (přednášející)
prof. RNDr. Antonín Kučera, Ph.D. (přednášející)
doc. Ing. Matej Lexa, Ph.D. (přednášející)
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Antonín Kučera, Ph.D.
Fakulta informatiky
Dodavatelské pracoviště: Fakulta informatiky
Předpoklady
!NOWANY( DEMBSY Embedded systems , DMKZI Quantum Information Processing , DPGZO Grafika a zpracování obrazu , DMPOS Metody počítačových sítí , DMZDD Zpracování digitálních dat , DPITS Podnikové IT systémy a služby , DZPJUI Metody ZPJ a UI , DPOSO Pokroky v souběžnosti , DRPSEC Research in comp.security )
Omezení zápisu do předmětu
Předmět je určen pouze studentům mateřských oborů.
Mateřské obory/plány
Cíle předmětu
Kurs je zaměřen na vybraná témata z oblasti formálních metod, jejichž důležitost a relevance již byla potvrzena četnými průmyslovými aplikacemi. Každé téma je prezentováno jako nezávislý výukový blok, který začíná krátkým úvodem v rozsahu 3-4 přednášek připravených lektorem. Po této úvodní části následují prezentace studentů, kteří referují o poznatcích nastudovaných v odborných článcích doporučených lektorem. Každý blok je zakončen diskusí, ve které jsou identifikována možná témata pro budoucí výzkum. Témata kurzu jsou volena především z následujících oblastí: stochastické procesy, stochastické programování a stochastické hry, metody a nástroje pro detekci chyb ve velkých programových systémech, formální modely a specifikační formalismy pro aplikace v oblasti mobilních sítí, hybridní systémy. Studium těchto pokročilých témat je doplněno krátkými kurzy vybraných partií matematiky (teorie pravděpodobnosti, diskrétní matematiky, matematické analýzy, numerických metod, atd.) zaměřených na vybudování potřebného aparátu.
Osnova
  • teorie pravděpodobnosti: stochastické procesy, Markovovy řetězce s diskrétním i spojitým časem, stochastické programování.
  • temporální logiky: logiky lineárního a větvícího se času, pravděpodobnostní rozšíření, model-checking
  • statická analýza: základní koncepty, analýza toku dat a toku řízení, aplikace a nástroje.
  • teorie her: základní pojmy a výsleky teorie her, min-max věta, Nashova věta, hry ve formální verifikaci, Martinova věta, stochastické hry
Literatura
  • KLEINBERG, Jon a Éva TARDOS. Algorithm design. Boston: Pearson/Addison-Wesley, 2006, xxiii, 838. ISBN 0321295358. info
  • PUTERMAN, Martin L. Markov decision processes : discrete stochastic dynamic programming. Hoboken, N.J.: Wiley-Interscience, 2005, xvii, 649. ISBN 0471727822. info
  • DAHLQUIST, Germund, Ned ANDERSON a Åke BJÖRCK. Numerical methods. Mineola, N.Y.: Dover Publications, 2003, xviii, 573. ISBN 0486428079. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • FILAR, Jerzy A. a Koos VRIEZE. Competitive Markov decision processes : with 57 illustrations. New York: Springer, 1997, xii, 393. ISBN 0387948058. info
  • NORRIS, J. R. Markov chains. 1st pub. Cambridge: Cambridge University Press, 1997, xvi, 237. ISBN 9780521481816. info
  • OWEN, Guillermo. Game theory. 3rd ed. San Diego: Academic Press, 1995, xii, 447. ISBN 0125311516. info
  • FELLER, William. An introduction to probability theory and its applications. 3rd ed. [New York]: John Wiley & Sons, 1968, xviii, 509. ISBN 9780471257080. info
Výukové metody
Přednášky, samostatné studium.
Metody hodnocení
Povinně volitelný předmět, ohodnocený 3 kredity, předmět lze opakovaně zapisovat.
Předmět je zařazen také v obdobích podzim 2007, jaro 2008, podzim 2008, jaro 2009, podzim 2009, jaro 2010, podzim 2010, jaro 2011, podzim 2011, jaro 2012, podzim 2012, jaro 2013, podzim 2013, podzim 2014, jaro 2015, podzim 2015, jaro 2016, podzim 2016, jaro 2017, podzim 2017, jaro 2018, podzim 2018, jaro 2019, podzim 2019, jaro 2020, podzim 2020.