Bakalářská práce

Vliv aproximací bit-vektorů na výkon nástroje Z3

Effect of Bit-Vector Approximations on the Performance of Z3

Dominika Krejčí, učo 445553
Anotace

Bakalářská práce se zabývá under-aproximacemi a over-aproximacemi kvantifikovaných bit-vektorových formulí a jejich vlivem na výkon SMT solveru Z3. V teoretické části rozebíráme problém splnitelnosti v teorii a aproximace bit-vektorů. V rámci praktické části byla vyhotovena implementace těchto aproximací pro SMT solver Z3 prostřednictvím Python API. Součástí je také vyhodnocení experimentálních výsledků vlivu aproximací na výkon nástroje Z3.

Abstract

In this thesis, we focus on under-approximations and over-approximations of quantified bit-vector formulae and their influence on the performance of SMT solver Z3. In the theoretical part, we analyze the problem of satisfiability modulo theory and approximations of bit-vectors. In the practical part, we implement these approximations for SMT solver Z3 using the Python API. Moreover, this thesis includes …více

Klíčová slova
splnitelnost v teorii aproximace bit-vektor Z3 SMT-LIB
Zadání práce
V nástroji Q3B se při řešení splnitelnosti kvantifikovaných formulí nad teorií bit-vektorů používají aproximace, které snižují bitovou šířku vybraných proměnných. Cílem bakalářské práce je vyhodnotit vliv těchto aproximací na výkon nástroje Z3. Tyto aproximace formulí mohou být pro nástroj Z3 implementovány pomocí API pro jazyk Python. Vyhodnocení musí být provedeno nad dostatečnou sadou kvantifikovaných formulí nad teorií bit-vektorů.
Administrativní informace
Práce zkontrolována:
29. 5. 2018 14:50, RNDr. Martin Jonáš, Ph.D., učo 359542
Plný text práce
464,9 KB / soubor PDF
Přílohy (2)
Jazyk práce
čeština čeština
Termín obhajoby
26. 6. 2018
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

RNDr. Jaroslav Bendík, Ph.D.
KTP FI MU

Konzultant

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

Literatura

  • JONÁŠ, Martin a Jan STREJČEK. Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. In Nadia Creignou and Daniel Le Berre. Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference. Berlin, Heidelberg: Springer, 2016, s. 267-283. ISBN 978-3-319-40969-6. Dostupné z: https://doi.org/10.1007/978-3-319-40970-2_17.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Aplikovaná 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.