IV101 - Seminář z verifikace (jaro 2013)
Náplň
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ů.
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ému a vypracují
verifikační projekt v rozsahu 15 hod.
Seminář
V jarním semestru 2013 jsou semináře rozvrhovány na pondělí od 13:00
do 14:50 v posluchárně B411. V týdnech dedikovaných práci na
projektu se seminář koná formou konzultací.
Požadavky na úspěšné ukončení
Pro úspěšné ukončení predmětu vyžadováno
vypracování úkolů v následujících dvou oblastech:
- Verifikace reálného kódu
Připravte podklady pro
realizaci jednoho vedeného cvičení/semináře v oblasti verifikace
reálného kódu s využitím jednoho z následujících verifikačních
nástrojů. Podklady typicky obsahují prováděcí slajdy/text,
demostrační příklady, zadání a řešení procvičovacích a domácích
úkolů.
- DiVinE
- Java Path Finder
- LLBMC
- CBMC
- Klee
- PEX
- Blast
- ... či jiný, po konzultaci s vyučujícím.
- Verifikace modelovaných systémů
Ve vámi zvoleném verifikačním nástroji vyřešte alespoň dva ze
tří projektů uvedených zde.
Úkoly se odevzdávají formou osobní prezentace vyučujícímu. Alespoň
jeden úkol musí být odevzdán (předveden) do 8.4.2013, druhý úkol musí
být předveden nejpozději do konce výuky semestru, tj. do 17.5.2013. V
případě nespokojenosti vyučujícího s kvalitou odevzdané práce, se
vyučující domluví se studentem na náhradním termínu odevzdání
opravené/zdokonalené verze. V případě nespokojenosti s odevzdaným
úkolem v náhradním termínu, či v případě neodevzdání úkolu v prvním
termínu, nemůže student předmět úspěšně absolvovat.
Jiri Barnat's Homepage