FI FMSA Formal Methods for Software Analysis
Název anglicky: Formal Methods for Software Analysis
v akred. studijním programu, prezenční, vyučovací jazyk: čeština čeština
Zahrnut v programu: FI C-TEV Tematické vzdělávání

Charakteristika plánu CŽV

  • Představení plánu CŽV (cíle vzdělávání)
    Studijní plán Formální metody pro analýzu software se zaměřuje na využívání matematických a logických metod k analýze, ověřování a zajištění správnosti softwarových systémů. Je zaměřen na teoretické a praktické techniky, které pomáhají detekovat chyby a nesprávnosti v softwarových systémech ještě před jejich nasazením do provozu, což zvyšuje bezpečnost, spolehlivost a efektivitu software.
  • Cílová skupina
    Studijní plán je ideální pro jednotlivce, kteří chtějí pracovat na vývoji bezpečných, spolehlivých a správně fungujících softwarových systémů, kde je minimální prostor pro chyby a kde formální metody mohou zásadně přispět k zajištění jejich kvality.
  • Další informace
  • Výstupy z učení

    Absolvent je odborník se silnými teoretickými i praktickými znalostmi v oblasti matematických a logických metod pro analýzu, verifikaci a ověřování softwarových systémů. Dokáže aplikovat algoritmy pro model checking, splnitelnost formulí
    a automatické dokazování k ověřování správnosti a bezpečnosti software.


    Má schopnost navrhovat a implementovat metody pro detekci chyb a nesprávností v kritických systémech, což je klíčové v oblastech, kde je vysoký požadavek na spolehlivost a bezpečnost, jako jsou letectví, automobilový průmysl, medicína nebo finance. Absolventi také chápou principy, schopnosti a omezení nástrojů pro automatizovanou verifikaci.

  • Uplatnění absolventa
    Absolventi jsou schopni efektivně analyzovat a zajišťovat kvalitu software pomocí pokročilých teoretických metod, což je klíčové pro odvětví, kde je software zásadní pro bezpečnost a stabilitu.
  • Podmínky přijetí
    Uchazeč je povinen doložit úspěšně ukončené středoškolské vzdělání a zaplatit poplatek za vzdělávání. Plán je nicméně doporučen pro absolventy alespoň bakalářského studia se zaměřením na matematiku nebo informatiku.
  • Průběh vzdělávání
    Jednotlivé předměty jsou vyučovány prezenčně. Očekává se tedy, že studenti se budou zúčastňovat výuky dle rozvrhu. Nad rámec přednášek a cvičení je možné poskytovat individuální konzultace.
  • Podmínky ukončení
    Předměty jsou ukončovány standardním způsobem, a to ověřováním nabytých znalostí závěrečným přezkoušením. Toto přezkoušení probíhá buď písemně či ústně. Forma ukončení je variabilní a záleží na zvoleném předmětu. V souladu se SZŘ MU jsou předměty ukončovány zápočtem, kolokviem či zkouškou.

Průchod plánem CŽV

Předměty CŽV

Kód Název Garant Ukončení Rozsah Kreditů Semestr
FI:IA085Satisfiability and Automated Reasoning M. Jonášzk 2/1/14+2 -
FI:IA159Formal Methods for Software Analysis J. Strejčekzk 2/0/02+2 -
FI:IA169Model Checking J. Strejčekzk 2/1/03+2 -
15 kreditů