Diplomová práce

Extending Concurrency Safety Checking in Slowbeast

Suyash Shandilya, učo 530727
Anotace

Slowbeast je efektivní symbolický exekutor schopný provádět různé úlohy ověřování programů. V této práci rozšiřujeme jeho funkčnost o možnost analyzovat souběžné programy na výskyt datových závodů. Používáme dynamickou redukci dílčích příkazů, abychom snížili počet prokladů, které je třeba pro analýzu souběžných programů prozkoumat. Naše výsledky porovnáváme se dvěma nejmodernějšími nástroji pro datovou …více

Abstract

Slowbeast is an efficient symbolic executor capable of performing various program verification tasks. In this work, we extend its functionality by enabling it to analyse concurrent program for data races. We use a dynamic partial order reduction to reduce the number of interleavings that need to be explored for concurrent program analysis. We compare our results with two state-of-the-art tools for …více

Klíčová slova
Slowbeast Symbolic execution data race detection formal verification model checking partial order reduction
Zadání práce
The goal of this thesis is to extend the abilities of the symbolic executor Slowbeast with checking for data races. The thesis will describe the problem of data-race detection, add a support for "no data race" property (as defined by SV-COMP rules) to Slowbeast, and extend Slowbeast to identify possible data races or their absence. Finally, the thesis will also contain an experimental comparison of Slowbeast and two state-of-the-art tools for data race detection on relevant benchmarks of SV-COMP 2024.
Administrativní informace
Práce zkontrolována:
18. 12. 2024 10:47, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
1 MB / soubor PDF
Přílohy (4)
Jazyk práce
angličtina angličtina
Termín obhajoby
3. 2. 2025
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

doc. RNDr. Petr Novotný, Ph.D., učo 172743
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Information Security

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.