IV101 Seminář z verifikace

Fakulta informatiky
jaro 2005
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející), prof. RNDr. Jiří Barnat, Ph.D. (zástupce)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Předpoklady
SOUHLAS
Omezení zápisu do předmětu
Předmět je určen pouze studentům mateřských oborů.

Předmět si smí zapsat nejvýše 12 stud.
Momentální stav registrace a zápisu: zapsáno: 0/12, pouze zareg.: 0/12
Mateřské obory/plány
předmět má 17 mateřských oborů, zobrazit
Cíle předmětu
Cílem semináře je získání praktických dovedností a zkušeností s automatizovanou verifikací zejména paralelních a distribuovaných systémů.
Osnova
  • V rámci semináře se studenti seznámí s několika nejpoužívanějšími verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systémů a vypracují verifikační projekt v rozsahu 15 hod. Seminář doplňuje předměty "Komunikace a paralelismus" a "Paralelní a distribuované výpočty".
Literatura
  • Peled, Doron. Software Reliability Methods. Springer, 2001.
  • HOLZMANN, Gerald J. The spin model checker :primer and reference manual. Boston: Addison-Wesley, 2004, xii, 596 s. ISBN 0-321-22862-6. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Informace učitele
http://www.fi.muni.cz/usr/brim/IV101
Další komentáře
Předmět je vyučován každý semestr.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.