Diplomová práce

Symbolic Execution with Predicate Abstraction in Slowbeast

Bc. Jindřich Sedláček, učo 514107
Anotace

Symbolická exekuce je algoritmus, který systematicky prohledává všechny proveditelné cesty v programu. Jeho hlavním omezením je, že počet proveditelných cest v programu může být neúnosně velký nebo dokonce nekonečný. Predikátová abstrakce je algoritmus, který nadhodnocuje chování programu pomocí uvažování nad konečnou množinou predikátů. Tato práce zkoumá nedávno navržený algoritmus, který kombinuje …více

Abstract

Symbolic execution is an algorithm that systematically explores all feasible program paths. Its major limitation is that the number of feasible program paths can be prohibitively large or even infinite. Predicate abstraction overapproximates program behaviour by reasoning about a finite set of predicates. This thesis explores a recently proposed algorithm that combines symbolic execution with predicate …více

Klíčová slova
Software Verification Symbolic Execution Predicate Abstraction CEGAR Slowbeast Symbiotic
Zadání práce
The goal of the thesis is to extend the symbolic executor Slowbeast with the recently proposed technique that combines symbolic execution and implicit predicate abstraction. The student will implement the technique and experimentally evaluate its effectiveness on a set of benchmarks from the International Competition on Software Verification (SV-COMP). The experimental evaluation should assess the effect both on standalone Slowbeast and also on Slowbeast when used as a part of the verification framework Symbiotic.
Administrativní informace
Práce zkontrolována:
5. 1. 2026 08:32, RNDr. Martin Jonáš, Ph.D., učo 359542
Plný text práce
966,9 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
30. 1. 2026
Práce byla úspěšně obhájena

Vedoucí

RNDr. Martin Jonáš, Ph.D., učo 359542
KTP FI MU

Oponent

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

Literatura

  • JONÁŠ, Martin; Jan STREJČEK a Alberto GRIGGIO. Combining Symbolic Execution with Predicate Abstraction and CEGAR. Online. In Nina Narodytska, Philipp Rümmer. Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024. Wien: TU Wien Academic Press, 2024, s. 272-280. ISBN 978-3-85448-065-5. Dostupné z: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_33.
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.