prof. Christoph Kirsch

Vedoucí Laboratoře výzkumu programování

Závěrečné práce

Bakalářské práce

Framework pro Vyhodnocování Rotor Modelů

Autor
Matěj Schrödl
Rok
2025
Typ
Bakalářská práce
Vedoucí
prof. Christoph Kirsch
Oponenti
prof. Jan Vitek, MSc., Ph.D.
Anotace
Tato práce je zaměřena na vytvoření platformy pro vyhodnocování SMT modelů vygenerovaných ze strojového kodu. Cílem práce je představit framework, který je schopen charakterizovat tyto modely, vyhodnocovat je pomocí různých SMT solverů a porovnávat je s konvenčnějšími SMT modely. Součástí práce je kromě vyvinutí této platformy také ukázka praktického využití na několika ukázkových srovnávacích testech. Tato platforma by měla pomoci v dalším vývojí oboru verifikace strojového kódu a sloužit jako nástroj pro analýzu SMT solverů.