Pierre Donat-Bouillud, Ph.D.

Závěrečné práce

Bakalářské práce

Symbolická exekuce pro R

Autor
Petr Šťastný
Rok
2024
Typ
Bakalářská práce
Vedoucí
Pierre Donat-Bouillud, Ph.D.
Oponenti
Ing. Sebastián Krynski, MSc.
Anotace
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í.

Diplomové práce

Vnořené smyčky a path explosion problém v symbolické exekuci

Autor
Vojtěch Rozhoň
Rok
2024
Typ
Diplomová práce
Vedoucí
Pierre Donat-Bouillud, Ph.D.
Oponenti
prof. Christoph Kirsch
Anotace
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í.