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

Validation of Violation Witnesses in Software Verification

Bc. Paulína Ayaziová, učo 485711
Anotace

V posledných rokoch sa generovanie svedkov spolu s výsledkom verifikačnej úlohy stalo bežnou praxou u nástrojov softvérovej verifikácie, keďže tieto svedky umožňujú automatické a nezávislé overenie verifikačného výsledku. Práca najprv rozoberá používaný generický formát verifikačných svedkov (formát 1.0) a poukazuje na niekoľko problémov súvisiacich s validáciou svedkov v tomto formáte pre programy …více

Abstract

Producing witnesses alongside the verdict for a verification task has become standard for software verifiers, as it allows for automatic and independent validation of the result. This work revisits the widely used generic format of verification witnesses, the witness format 1.0, and shows several problems in its definition related to the validation of witnesses for C programs. These issues motivated …více

Klíčová slova
software verification verification witnesses witness-based validation symbolic execution program analysis
Zadání práce
The thesis will focus on violation witnesses in verification of C programs. The first goal is to summarize issues of the Witness Format 1.0 and present the Witness Format 2.0, in particular its part for violation witnesses. The main goal of the thesis is to implement a witness validator for violation witnesses in the format 2.0. The validator will be based on symbolic execution. The thesis will also present an experimental evaluation of the new validator and a comparison with CPAchecker.
Administrativní informace
Práce zkontrolována:
23. 5. 2024 10:58, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
2 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
21. 6. 2024
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
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Formální analýza počítačových systémů

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.