Pierre Donat-Bouillud, Ph.D.

Pierre Donat-Bouillud, Ph.D.

Sebastián Krynski, MSc.

Katedra teoretické informatiky

Symbolic execution je technika, která umožňuje testovat programy a dokazovat jejich netriviální vlastnosti. Vytvoření nového systému pro symbolic execution je náročné. Místo toho je použita technika, kdy je symbolicky spouštěn samotný interpret cílového jazyka, díky čemuž je jednodušší symbolicky spustit i programy v daném jazyce. V této práci aplikuji tuto techniku na jazyk R. Výsledný program je možné použít například na otestování korektnosti knihoven nebo na generování typových anotací.

Práce na DSpace

Pierre Donat-Bouillud, Ph.D.

Ing. Stanislav Kuznetsov, Ph.D.

Katedra softwarového inženýrství

Automatizované systémy hodnocení pro programovací kurzy čelí výzvám v oblasti zabezpečení a testovací přísnosti, zejména u pokročilých témat, jako jsou nástroje pro testování programů. Tato práce představuje Fittest, nový automatizovaný systém hodnocení navržený k řešení těchto výzev. Využívá bezpečnou hybridní architekturu, kde studentský kód běží v GitLab CI, ale kritická logika hodnocení probíhá na chráněném backendovém serveru. Fittest podporuje dynamické generování programů v jazyce C pro hodnocení studenty vyvinutých nástrojů pro pokrytí kódu a fuzzerů a integruje se s ověřováním na univerzitě. Výsledkem je bezpečná a pedagogicky podložená platforma pro hodnocení kurzu NI-APT.

Pierre Donat-Bouillud, Ph.D.

Ing. Petr Máj, Ph.D.

Katedra softwarového inženýrství

Tato práce se zabývá kritickou výzvou reprodukovatelnosti ve výpočetním výzkumu prováděném pomocí notebooků v jazyce R. Ačkoli notebooky v jazyce R způsobily revoluci ve vědeckých pracovních postupech integrací kódu, narativu a výsledků, jejich výstupy se často liší v různých prostředích kvůli závislosti na verzích knihoven, operačních systémech a časově závislých operacích. Tradiční nástroje pro porovnávání, jako je GNU Diff, nedokážou zachytit smysluplné rozdíly v dynamických výstupech, jako jsou grafy a statistické tabulky. Tento výzkum vyvíjí a hodnotí nástroj pro sémantické porovnávání speciálně navržený pro notebooky v jazyce R, který dokáže detekovat rozdíly nad rámec textového porovnání. Prostřednictvím komplexní analýzy programovacího jazyka R a ekosystému notebooků byl implementován nástroj, který počítá metriky podobnosti (včetně DSSIM a relativního rozdílu) pro výstupy, u kterých se předpokládá, že jsou sémanticky ekvivalentní. Hodnocení v různých výpočetních prostředích prokázalo schopnost nástroje identifikovat smysluplné rozdíly, které by konvenční textové porovnávání přehlédlo, zejména u složitých výstupů, jako jsou vizualizace dat a statistické tabulky. Navzdory jeho účinnosti stále existují příležitosti ke zlepšení výpočetní efektivity, zejména v rychlosti generování výstupů a optimalizaci výpočetní fáze shora dolů. Tato práce přispívá k vědě o reprodukovatelnosti tím, že umožňuje sofistikovanější porovnávání výstupů notebooků, zvyšuje transparentnost a spolehlivost ve výpočetním výzkumu.

Pierre Donat-Bouillud, Ph.D.

prof. Christoph Kirsch

Katedra teoretické informatiky

Práce vyhodnocuje techniky pro řešení problému exploze cest v symbolické exekuci. Obzvláštní důraz je kladen na interakce jednotlivých technik se vnořenými cykly. Metody ořezávání cest, subsumpce cest, slučování stavů a shrnování cyklů jsou diskutovány na příkladech. Symbolická exekuce je spolu s těmito metodami implementována pro analýzu programů napsaných v edukačním programovacím jazyce microc, který je inspirován jazykem C. Práce představuje experimenty, které porovnávaly jednotlivé metody, obzvláště aby zjistili jak dobře se tyto metody vypořádávají s mnoha cykly a se vnořenými cykly. Generátor náhodných programů v jazyce microc byl implementován pro experimentování s implementovanou symbolickou exekucí.

Práce na DSpace

Pierre Donat-Bouillud, Ph.D.

Ing. Josef Gattermayer, Ph.D.

Katedra teoretické informatiky

Vyper je programovací jazyk pro psaní smart kontraktů pro EVM blockchainy. Smart kontrakty mohou držet až miliardy dolarů, a proto je jejich bezpečnost nejvyšší prioritou. V minulosti Vyper kompilátor obsahoval bugy, které ovlivňovaly produkční kontrakty a nakonec vedly k rozsáhlému hackerskému útoku. Tato práce se zabývá tématem testování kompilátorů se zaměřením na testování Vyper kompilátoru. Implementuje AST interpret pro Vyper a používá jej k diferenciálnímu fuzzování překladače. Přístup je testován pomocí experimentů proveditelnosti, kdy jsou dvě staré chyby Vyperu s vysokou a střední závažností přeneseny do aktuální verze a fuzzer je zaměřen na jejich nalezení. Experimenty ukázaly, že fuzzer je dokáže rychle odhalit, a lze jej tedy použít ke zlepšení správnosti překladače.

Práce na DSpace