IV101 - Seminář z verifikace (jaro 2012)
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 2012 jsou semináře rozvrhovány na pondělí od 12:00
do 13:50 v posluchárně C408. V týdnech dedikovaných práci na
projektu se seminář koná formou konzultací.
Požadavky na úspěšné ukončení
V semestru Jaro 2012 je pro úspěšné ukončení predmětu vyžadováno
vypracování úkolů v následujících dvou oblastech:
- 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.
- 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
- CBMC
- Klee
- PEX
- Blast
- ... či jiný, po konzultaci s vyučujícím.
Úkoly se odevzdávají formou osobní prezentace vyučujícímu. Alespoň
jeden úkol musí být odevzdán (předveden) do 16.4.2012, druhý úkol musí
být předveden nejpozději do konce výuky semestru, tj. do 18.5.2012. 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