Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Fiedor Jan, Ing.
Topic:Practical Methods of Automated Verification of Concurrent Programs
Start:2009/2010
Date of Defense:2017-06-23
Title of Dissertation:Practical Methods of Automated Verification of Concurrent Programs
PhD thesis subject:

Automatizovaná verifikace počítačových systémů je v současnosti velmi živě se rozvíjející oblastí. Předmětem disertační práce je konkrétně verifikace paralelních počítačových programů, a to s důrazem na paralelní programy v Javě. V rámci výzkumu budou uvažovány přístupy založené na statické analýze, model checkingu i dynamické analýze. Jejich rozvoj bude motivován snahou dosáhnout jejich co nejvyšší praktičnosti, proto bude výrazně řízen snahou pracovat s konkrétními případovými studiemi. Významné výzkumné úsilí bude rovněž zaměřeno na kombinace různých přístupů k verifikaci paralelních systémů s cílem tímto způsobem výrazně zvýšit jejich efektivitu. Budou také zkoumány možnosti úpravy stávajících nebo návrhu nových technik vhodných pro verifikaci systémů s méně studovanými, ale přesto (zejména v souvislosti s nástupem masového paralelismu) významnými synchronizačními prostředky jako jsou bariéry, bez-zámkové struktury apod. Uvedené metody mohou být studovány i s přihlédnutím k případným možnostem automatických oprav nalezených chyb.

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou verifikací v rámci výzkumného záměru MŠMT ČR MSM0021630528 "Výzkum informačních technologií z hlediska bezpečnosti", grantů GA ČR 102/07/0322 "Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů", Barrande/Kontakt MEB 020840 "Pokročilé techniky automatické verifikace nekonečně stavových systémů" a případných dalších projektů, které se v této oblasti podaří získat.

V rámci práce je možnost stáží na vybraných zahraničních pracovištích spolupracujících úzce s VeriFIT (IBM Haifa Research Laboratory, Uppsala, Verimag Grenoble, LIAFA Paříž apod.) zaměřených na aktivní spolupráci na výzkumu ve vytyčené oblasti. Předpokládá se aktivní účast na vybraných mezinárodních konferencích zaměřených v souladu s tématem práce.

Part of research project: