Diplomová práce

Compact Symbolic Execution in Slowbeast

Bc. Kristián Kumor
Anotace

Symbolická exekúcia sa používa na generovanie testov alebo na softvérovú verifikáciu. Funguje tak, že namiesto konkrétnych vstupov pre program používa symboly a skúma všetky možné cesty v programe. Trpí však problémom explózie ciest, ktorý je spôsobený vetvením ciest v programe. To spôsobuje, že klasický prístup nie je optimálny, pretože skúmanie niektorých ciest je nadbytočné. Cieľom tejto práce je …více

Abstract

Symbolic execution is generally used for generating tests or for software verification. It works by using symbols instead of concrete program inputs and exploring all possible execution paths in a program. However, it suffers from the path explosion problem caused by path forking. This makes the classical approach suboptimal, as exploring some of the execution paths is not feasible. This work aims …více

Klíčová slova
Slowbeast Symbolic execution Compact symbolic execution Path explosion problem Formal verification Program analysis SMT-solving
Zadání práce
The main goal of the thesis is extending the symbolic executor Slowbeast with "compact symbolic execution" technique to speed up symbolic execution on programs with loops. Slowbeast is a part of the program analysis and verification framework called Symbiotic. Another goal of the thesis is to modify the configuration of Symbiotic such that it employs the compact symbolic execution implemented in Slowbeast. After implementation, the student will perform performance comparisons for Symbiotic with integrated Slowbeast, with and without symbolic execution, on benchmarks from SV-COMP 2024.
Administrativní informace
Práce zkontrolována:
23. 5. 2024 11:01, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
597 KB / soubor PDF
Přílohy (2)
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

RNDr. Petr Ročkai, Ph.D., učo 139761
KPSK FI MU

Konzultant

Mgr. Marek Trtík, Ph.D., učo 329313
KVI FI MU

Literatura

  • SLABÝ, Jiří; Jan STREJČEK a Marek TRTÍK. Compact Symbolic Execution. In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Berlin Heidelberg: Springer, 2013, s. 193-207. ISBN 978-3-319-02443-1. Dostupné z: https://doi.org/10.1007/978-3-319-02444-8_15.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Principy programovacích jazyků

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.