Bakalářská práce

Paralelní volání SMT solverů v nástroji Bugst

Parallel calls of SMT solvers in Bugst

Viktor Toman, učo 396026
Anotace

Symbolická exekúcia je metóda analýzy programov, ktorá produkuje otázky vo forme formulí prvého rádu. Symbolické exekútory používajú SMT riešiče na rozhodovanie splniteľnosti týchto formulí vzhľadom na teórie na pozadí. Rozličné SMT riešiče majú rozličné silné stránky, a používanie viacerých SMT riešičov v symbolickom exekútore môže zlepšiť jeho výkon. Ciele tejto práce sú integrácia dvoch ďalších …více

Abstract

Symbolic execution is a program analysis method that produces queries in form of first-order formulas. Symbolic executors use SMT solvers to decide satisfiability of these formulas modulo background theories. Different SMT solvers have different strengths and using multiple SMT solvers in a symbolic executor can improve its performance. The goals of this thesis are integration of two additional SMT …více

Klíčová slova
program analysis symbolic execution SMT solving SMT solver parallel calls
Zadání práce
Bugst je open-source nástroj pro analýzu programů pomocí symbolické exekuce, který momentálně používá k rozhodování splnitelnosti formulí pouze SMT solver Z3. Prvním cílem práce je napojit Bugst i na další dva SMT solvery dle vlastního výběru. Druhým cílem je implementace paralelního volání vícero SMT solverů a ukončení jejich běhu po obdržení prvního relevantního výsledku. Součástí práce budou i experimenty, které porovnají, jak ovlivňuje použitý SMT solver nebo jejich paralelní kombinace výkon Bugstu.
Administrativní informace
Práce zkontrolována:
20. 5. 2014 10:39, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
447,9 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
16. 6. 2014
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

Mgr. Marek Trtík, Ph.D., učo 329313
KPSK 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.