Práce je nadprůměrně náročná mj. s ohledem na to, že staví na metodách statické analýzy, které nejsou předmětem bakalářského studia na FIT VUT. Práce také vyžadovala pokročilé funkcionální programování v jazyce Ocaml, v němž je napsáno prostředí Meta Infer. Bylo rovněž zapotřebí seznámení se s prostředím Infer, které není příliš detailně zdokumentováno. Práce vyžadovala návrh originálního přístupu k analýze zaměřené na souběhy nad daty („data race“) způsobem kompatibilním s tím, že prostředí Meta Infer analyzuje programy zdola nahoru dle stromu volání, což vede na analýzu každé jednotlivé funkce bez znalosti kontextu jejího volání. Známé analýzy daného typu dostupné v literatuře přitom pracují dle stromu volání shora dolů.

Studentka začala v dané oblasti pracovat v rámci projektové praxe a její práce je významná pro několik výzkumných projektů řešených ve skupině VeriFIT (mj. GAČR AIDE či HE Chess). S dosaženými výsledky jsem velmi spokojen. Vytvořený nástroj poskytuje slibné výsledky a po dalším dopracování, o které studentka již projevila zájem, je zde potenciál k publikaci na kvalitní mezinárodní konferenci minimálně formou článku o nástroji.

Jak již bylo řečeno, studentka začala na tématu pracovat již v rámci projektové praxe. Po celou dobu řešení byla velmi aktivní, účastnila se pravidelných schůzek skupiny, prezentovala dosažené pokroky i možnosti dalšího pokračování práce a řešení různých problémů, které se při práci objevily.

Práce byla úspěšně prezentována na studentské konferenci Excel@FIT, kde získala Cenu firmy Honeywell, Cenu firmy NXP a ocenění odbornou veřejností – Cenu Jiřího Kunovského. Předpokládáme, že po dalším dopracování by měl být vytvořený nástroj publikován formou článku o nástroji na některé z uznávaných mezinárodních konferencí v dané oblasti. Vytvořený nástroj DARC je k dispozici jako open source.

Za zmínku stojí také to, že studentka v rámci studijní části své práce pomohla s přípravou publikace o dříve vytvořeném statickém analyzátoru L2D2, zaměřeném na vyhledávání uváznutí, na mezinárodní konferenci EUROCAST 2022 se sborníkem vydaným v edici LNCS nakladatelství Springer a je spoluautorkou této publikace.

Stupeň hodnocení: značně obtížné zadání

Navržená analýza je založena na abstraktní interpretaci, jenž vyžaduje od studenta znalosti z oblastí matematiky, teoretické informatiky, a formální analýzy a verifikace. S předměty pokrývajícími tyto oblasti se studenti setkávají až v rámci magisterského studia, pro studenta bakalářského studia je tedy výrazně obtížnější tuto problematiku pochopit. Implementace analýzy ve formě zásuvného modulu pro nástroj Meta Infer navíc vyžaduje použití funkcionálního jazyka OCaml, se kterým se student během bakalářského studia také nesetká a klade to na něj další nároky.

Pro studenta bakalářského studia pokládám tedy toto téma za velmi náročné.

Stupeň hodnocení: přesahuje obvyklé rozmezí

Práce mírně přesahuje obvyklé rozmezí. Důvodem je obtížnost tématu, jenž vyžaduje podrobné uvedení do problematiky a detailní popis návrhu řešení i implementace. Práce navíc vhodně doplňuje popis návrhu a implementace konkrétními ukázkami na příkladech, což velmi usnadňuje čtenáři pochopení dané problematiky i navrženého řešení.

Práce je psána v anglickém jazyce s minimem překlepů nebo chyb. Typograficky je práce na úrovni vědeckých článků a jiných odborných publikací.

Navržená analýza je implementována ve formě zásuvného modulu pro nástroj Meta Infer, je plně funkční, a výkonnostně srovnatelná s existujícími řešeními.

Funkčnost navržené analýzy byla otestována na třech testovacích sadách (vlastní vytvořené sadě ConcurrencyBenchmark, veřejné testovací sadě DataRacebenchmark a testovací sadě z mezinárodní soutěže analýzy software SV-COMP) a srovnána s několika existujícími nástroji pro odhalování chyb v souběžnosti (data race). Pro ověření škálovatelnosti byla následně analýza otestována na několika reálných aplikacích včetně eProsima/Fast-DDS čítající přes 100 000 řádků kódu.