IV101 Seminář z verifikace

Fakulta informatiky
jaro 2015
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, 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
Po 16:00–17:50 C416
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 35 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í počítačových systémů. V rámci semináře se studenti seznámí s několika verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systému a připraví prezentaci vybraného verifikační nástroje a prezentují jej ostatním studentům v prezentaci o rozsahu cca dvou vyučovacích hodin.
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 připraví prezentaci vybraného verifikačního nástroje.
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
Výukové metody
teoretická příprava, příprava prezentace, prezentace
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na prezentaci.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Studijní materiály
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2013
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, 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
Po 13:00–14:50 B411
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 37 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í počítačových systémů. Konkrétně by studenti po absolvování tohoto kurzu měli být schopni smysluplně použít většinu standardních nástrojů pro ověřování modelu, jako jsou DiVinE, SPIN, UPPAAL, nebo PRISM.
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.
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
Výukové metody
teoretická příprava, práce na projektu
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Studijní materiály
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2012
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, 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
Po 12:00–13:50 C408
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 37 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í počítačových systémů. Konkrétně by studenti po absolvování tohoto kurzu měli být schopni smysluplně použít většinu standardních nástrojů pro ověřování modelu, jako jsou DiVinE, SPIN, UPPAAL, nebo PRISM.
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.
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
Výukové metody
teoretická příprava, práce na projektu
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Studijní materiály
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2010
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 12:00–13:50 B411
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 36 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í počítačových systémů. Konkrétně by studenti po absolvování tohoto kurzu měli být schopni smysluplně použít většinu standardních nástrojů pro ověřování modelu, jako jsou DiVinE, SPIN, UPPAAL, nebo PRISM.
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.
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
Výukové metody
teoretická příprava, práce na projektu
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
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 podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2009
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 12:00–13:50 B411
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 33 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í počítačových systémů. Konkrétně by studenti po absolvování tohoto kurzu měli být schopni smysluplně použít většinu standardních nástrojů pro ověřování modelu, jako jsou SPIN, UPPAAL, nebo PRISM.
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.
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/~xbarnat/IV101/
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2008
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Předpoklady
SOUHLAS
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 37 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.
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/~xbarnat/IV101/
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2007
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 14:00–15:50 B411
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.
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/~xbarnat/IV101/
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
podzim 2005
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Rozvrh
St 8:00–9:50 B411
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.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

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.

IV101 Seminář z verifikace

Fakulta informatiky
podzim 2004
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
prof. RNDr. Luboš Brim, CSc. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Rozvrh
každý lichý čtvrtek 14:00–17:50 B003
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.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2004
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející)
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
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.
  • 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, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
podzim 2003
Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející)
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
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.
  • 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 jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2019

Předmět se v období jaro 2019 nevypisuje.

Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, 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
Předpoklady
IV113 Úvod do validace a verifikace
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 36 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í počítačových systémů. V rámci semináře se studenti seznámí s několika verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systému a připraví prezentaci vybraného verifikační nástroje a prezentují jej ostatním studentům v prezentaci o rozsahu cca dvou vyučovacích hodin.
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 připraví prezentaci vybraného verifikačního nástroje.
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
Výukové metody
teoretická příprava, příprava prezentace, prezentace
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na prezentaci.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2018

Předmět se v období jaro 2018 nevypisuje.

Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, 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
Předpoklady
IV113 Úvod do validace a verifikace
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 36 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í počítačových systémů. V rámci semináře se studenti seznámí s několika verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systému a připraví prezentaci vybraného verifikační nástroje a prezentují jej ostatním studentům v prezentaci o rozsahu cca dvou vyučovacích hodin.
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 připraví prezentaci vybraného verifikačního nástroje.
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
Výukové metody
teoretická příprava, příprava prezentace, prezentace
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na prezentaci.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2017

Předmět se v období jaro 2017 nevypisuje.

Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, 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
Předpoklady
IV113 Úvod do validace a verifikace
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 36 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í počítačových systémů. V rámci semináře se studenti seznámí s několika verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systému a připraví prezentaci vybraného verifikační nástroje a prezentují jej ostatním studentům v prezentaci o rozsahu cca dvou vyučovacích hodin.
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 připraví prezentaci vybraného verifikačního nástroje.
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
Výukové metody
teoretická příprava, příprava prezentace, prezentace
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na prezentaci.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2016

Předmět se v období jaro 2016 nevypisuje.

Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, 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
Předpoklady
IV113 Úvod do validace a verifikace
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 36 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í počítačových systémů. V rámci semináře se studenti seznámí s několika verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systému a připraví prezentaci vybraného verifikační nástroje a prezentují jej ostatním studentům v prezentaci o rozsahu cca dvou vyučovacích hodin.
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 připraví prezentaci vybraného verifikačního nástroje.
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
Výukové metody
teoretická příprava, příprava prezentace, prezentace
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na prezentaci.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2014

Předmět se v období jaro 2014 nevypisuje.

Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, 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
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 35 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í počítačových systémů. Konkrétně by studenti po absolvování tohoto kurzu měli být schopni smysluplně použít většinu standardních nástrojů pro ověřování modelu, jako jsou DiVinE, SPIN, UPPAAL, nebo PRISM.
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.
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
Výukové metody
teoretická příprava, práce na projektu
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2011

Předmět se v období jaro 2011 nevypisuje.

Rozsah
0/2. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
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, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 36 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í počítačových systémů. Konkrétně by studenti po absolvování tohoto kurzu měli být schopni smysluplně použít většinu standardních nástrojů pro ověřování modelu, jako jsou DiVinE, SPIN, UPPAAL, nebo PRISM.
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.
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
Výukové metody
teoretická příprava, práce na projektu
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
jaro 2003

Předmět se v období jaro 2003 nevypisuje.

Rozsah
0/2. 2 kr. (plus ukončení). Ukončení: z.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
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 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20
Mateřské obory/plány
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.
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
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, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.

IV101 Seminář z verifikace

Fakulta informatiky
podzim 2002

Předmět se v období podzim 2002 nevypisuje.

Rozsah
0/2. 2 kr. (plus ukončení). Ukončení: z.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
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 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20
Mateřské obory/plány
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.
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
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, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2015.