Bakalářská práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

Klee-Based Error Witness Checker

Paulína Ayaziová, učo 485711
Anotace

Keďže verifikačné nástroje občas produkujú nekorektné výsledky, generovanie svedkov sa stalo bežnou súčasťou verifikácie softvéru. Táto práca sa zaoberá svedkami chýb v programoch. V práci popisujeme používaný formát týchto svedkov a nástroje slúžiace na ich overenie. Ako hlavný výsledok práce predstavujeme nový nástroj na overovanie svedkov, Witch-Klee, založený na symbolickej exekúcii. Tento nástroj …více

Abstract

Providing witnesses has become a standard practice in software verification, as software verifiers occasionally produce incorrect results. This thesis focuses on witnesses of erroneous behaviour. We describe the commonly used format of software verification witnesses and present the currently available error witness checkers and their validation techniques. As the primary outcome, we introduce a new …více

Klíčová slova
symbolic execution software verification verification witnesses program analysis Klee witness validation
Zadání práce
Cílem práce je vytvořit nástroj pro ověřování svědků chybového chování programů, který bude založen na symbolickém exekutoru Klee. Nástroj bude podporovat formát svědků založený na GraphML používaný v soutěži SV-COMP. Součástí práce bude přehled existujících nástrojů pro ověřování svědků a porovnání nově vzniklého nástroje s vybranými existujícími nástroji na svědcích z SV-COMP 2021.
Administrativní informace
Práce zkontrolována:
17. 12. 2021 01:09, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
2,5 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
8. 2. 2022
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU

Oponent

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Konzultant

RNDr. Marek Chalupa, Ph.D.
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.