Software Verification and Testing

The specialization Software Verification and Testing is open in Czech language only.

Cílem specializace Verifikace a testování software je seznámit studenty s technikami pro zajištění kvality počítačových systémů. Během studia se student seznámí s technikami statické analýzy a verifikace, automatizovaného testování, modelování systémů a se základy bezpečnosti. V rámci obecných předmětů pak student dále získá rozhled v oblasti teoretických základů informatiky, matematické statistiky a pravděpodobnosti, umělé inteligence a strojového učení, nebo  ukládání dat. Díky kvalitnímu teoretickému vzdělání a širokému univerzálnímu základu aplikačně zaměřeného oborového studia je přitom zajištěna vysoká adaptabilita absolventa na mnohé aktuální požadavky jeho budoucí profesionální praxe, a to i v jiných oblastech informačních technologií.

• Absolvent se orientuje v oblasti technik pro zajištění kvality (nejen) software. Konkrétně má přehled o technikách automatizovaného testování a dynamické analýzy, statické analýzy a verifikace a technikách založených na tvorbě modelů, jejich simulace a analýzy. Kromě toho má přehled i v oblasti zajištění bezpečnosti informačních technologií.
• Absolvent je připraven na samostatnou práci v oblasti navrhování testů a statických metod za účelel hledání chyb a zajištění bezproblémového běhu počítačových systémů. S ohledem na široký teoretický základ oboru Informační technologie a umělá inteligence má možnost uplatnění i v dalších oblastech návrhu, vývoje a výzkumu informačních technologií.
• Absolvent se může uplatnit v quality ensurance týmech velkých projektů a to jak na pozici návrháře testů (test architect), manažera kvality, nebo vedoucího týmu. Dále se pak mohou uplatnit v research and developement týmech velkých firem zaměřených na automatizovanou analýzu software. Specializace je ale i výborným základem pro práci vedoucího týmu vývojářů, nebo systémového architekta. V neposlední řadě umožňuje absolventům pracovat v oblasti výzkumu a inovací v oblasti automatizované analýzy a verifikace.

Státní zkouška programu Informační technologie a umělá inteligence, specializace Verifikace a testování software se skládá z částí:

• prezentace a obhajoba zpracované diplomové práce,
• ústní zkoušky, která sdružuje základní tematické okruhy obsažené v předmětech profilujícího základu z oblasti Informačních technologií a umělé inteligence (Teoretická informatika, Statistika a pravděpodobnost, Architektury výpočetních systémů, Umělá inteligence a strojové učení, Ukládání a příprava dat, Funkcionální a logické programování, Paralelní a distribuované algoritmy, Moderní trendy informatiky),
• ústní zkoušky, která sdružuje základní tematické okruhy obsažené v předmětech profilujícího základu z oblasti Testování a verifikace software (Analýza systémů založených na modelech, Automatizované testování a dynamická analýza, Statická analýza a verifikace, Systémy odolné proti poruchám, Simulační nástroje a techniky, Bezpečnost informačních systémů).

Všechny části státní zkoušky se konají ve stejném termínu před komisí pro státní zkoušky. Ke státní zkoušce může přistoupit student, který získal potřebný počet kreditů v předepsané skladbě nutný pro úspěšné ukončení magisterského studia a odevzdal diplomovou práci v řádném termínu. Organizace a průběh státní zkoušky jsou dány odpovídající vnitřní normou fakulty a příslušnými pokyny garanta programu ke státním zkouškám.

• Statická analýza v nástroji Facebook Infer zaměřená na detekci uváznutí 
• Statická analýza programů s dynamickými datovými strukturami a další datovými typy v 2LS 
• Refaktoring a verifikace kódu mkfs xfs
• Generování modelů pro testy ze zdrojových kódů
• Ověřování temporálních vlastností konečných běhů programů
• Generování testovacích vstupů podle stopy programu
• Syntéza důkazů nekonečnosti běhu programů s využitím šablon
• Abstrakce dynamických datových struktur s využitím šablon
• Generátor testovacích běhů nad GUI
• Generická syntéza invariantů v programu založená na šablonách
• Prostředí pro analýzu paralelních C/C++ programů
• Automatická detekce degradace výkonu