Tomáš Dacík má podle svých slov rád zdánlivě neřešitelné problémy a nevadí mu být slovy Járy Cimrmana průkopník slepých uliček. „V kontextu mé doktorské práce jako celku nepředpokládám, že bych skončil ve slepé uličce. Podobné výzkumy už totiž existují. Ale samozřejmě člověk v průběhu naráží na dílčí matematické či programátorské problémy, u kterých předem neví, jakým směrem se vydat. V takovém případě musím prostě vyzkoušet řadu možností a počítat s tím, že většina budou slepé cesty. Občas je to frustrující, ale to spíše výjimečně,” říká Tomáš Dacík z FIT VUT.

Dodává, že jeho práce je tak hodně o experimentech a experimentálním měření. „V tom je velká výhoda informatiky. Experimentální ověření si můžu spustit přímo u sebe na počítači. Nepotřebuju drahé přístroje, laboratoře, chemikálie,” podotýká.

Ve své práci se věnuje statické analýze programů. „To znamená, že ověřuju vlastnosti programů bez toho, aby se daný program musel spouštět. Napíše se jiný program zkoumající ten, který nás zajímá. Vlastnosti programů lze ověřovat i dynamicky. Program se spustí a sleduje se, co dělá. Jestli v něm nedochází k chybám, jestli neběží příliš pomalu,” přibližuje zjednodušeně Dacík. Podle něj ale dynamické ověřování není příliš efektivní, protože se prozkoumá pouze jeden běh programu.

Tomáš Dacík se pak konkrétně věnuje analýze programů, které pracují s dynamicky alokovanou pamětí. „To znamená, že program dopředu neví, kolik paměti bude potřebovat. Paměť se přiděluje až za běhu,” popisuje. Právě v tomto typu programů se pak mohou objevovat chyby, které se projeví pouze v určitých operačních systémech, nebo se neobjevují pravidelně, ale pouze nahodile. „V takovém případě pak spustíme program jednou a vypadá to, že je vše v pořádku. Když se ale spustí podruhé, tak třeba za běhu spadne. To je důvod, proč jsou takové chyby nepříjemné. Druhý a zcela zásadní aspekt je bezpečnost. Tyto chyby jsou totiž často zdrojem bezpečnostních zranitelností,” upozorňuje Dacík. Často tyto bezpečnostní zranitelnosti mohou být v prohlížečích. „Ty používá každý z nás a jsou dost kritické, protože prohlížečům například svěřujeme svá hesla. Podle analýz Microsoftu a Googlu má až 70 procent chyb původ v práci s dynamicky alokovanou pamětí,” dodává Tomáš Dacík.

Jeho práce je zatím ve fázi základního výzkumu a věnuje se tomu, jak reprezentovat konfiguraci těchto programů, k čemuž používá separační logiku. „Z pohledu programátora se to dá představit jako datová struktura, která efektivním způsobem umožňuje popisovat nekonečné množiny paměťových konfigurací. Zjednodušeně se věnuju návrhu operací nad datovou strukturou,” říká. V druhé části by pak chtěl metody začlenit do analyzátoru programů Broom, který vyvíjí výzkumná skupina VeriFIT na FIT VUT ve spolupráci s TU Wien, a případně do některého dalšího nástroje. „Navazuju na diplomovou práci, kterou bych chtěl zdokonalit a výsledky dotáhnout tak, aby byly opravdu využity v rámci nějakého analyzátoru programů. Z dlouhodobého hlediska bych pak chtěl přispět k tomu, aby se téma posunulo z akademické sféry do průmyslové,” dodává.

Jeho výzkum i dosavadní výsledky natolik zaujaly odbornou komisi, že se Tomáš Dacík letos zařadil mezi oceněné doktorské studenty v rámci Brno Ph.D. Talent. „Byla to pro mě velmi zajímavá zkušenost. Finální prezentace jsou velmi krátké, takže člověk musí vyladit každý jeden slide a musí mluvit k věci a jasně. Zároveň jsou v komisi jak akademici, tak lidé z firem, takže je musí přesvědčit nejen o kvalitě svého výzkumu, ale i využitelnosti v praxi. To, že jsem byl nakonec oceněný a dostal jsem stipendium, beru jako motivaci a potvrzení, že svou práci dělám dobře. Zároveň je to i závazek v tom pokračovat,” uzavírá Tomáš Dacík.

(zeh)