Bakalářská práce

Implementation of 3-valued BDDs in Q3B

Matěj Pavlík, učo 469088
Anotace

Práce se zabývá SMT-solverem Q3B pracujícím nad teorií kvantifikovaných bitvektorových formulí, který reprezentuje průběžné výsledky pomocí binárních rozhodovacích diagramů (BDD). Q3B využívá aproximace množiny modelů dvojicí diagramů -- nadhodnocujícího a podhodnocujícího. V práci je tato reprezentace nahrazena jediným diagramem s novým cílem ? (vedle původních 0, 1), což může potenciálně vést k nižším …více

Abstract

The thesis deals with the Q3B SMT-solver working over the theory of quantified bit-vector formulas, which represents the intermediate results using binary decision diagrams (BDDs). Q3B employs approximations of the set of models with a pair of BDDs -- overapproximating and underapproximating. In the works, the representation is replaced with a single BDD with a new target ? (besides the original 0 …více

Klíčová slova
binary decision diagrams (BDDs) CUDD 3-valued BDDs bit-vectors Q3B SMT-solving
Zadání práce
Q3B is an SMT solver for quantified bitvector formulas, which is based on manipulating binary decision diagrams (BDDs) using the CUDD library. Internally, the solver uses pairs of BDDs representing under- and overapproximations of the set of satisfying valuations. The aim of this work is to introduce 3-valued BDDs containing a special target value "?" for "unknown" (besides the original 1 and 0) into the CUDD library which would allow to merge the pairs into single BDDs. The implementation will support all basic operations on 3-valued BDDs such as AND, XOR, ITE as well as bit-vector operations. Also, the Q3B solver will be modified so that it employs 3-valued BDDs. The work will also provide an experimental comparison of the new approach against the original implementation.
Administrativní informace
Práce zkontrolována:
31. 5. 2021 10:21, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
690,6 KB / soubor PDF
Přílohy (2)
Jazyk práce
angličtina angličtina
Termín obhajoby
29. 6. 2021
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
KTP FI MU

Konzultant

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

Literatura

  • JONÁŠ, Martin a Jan STREJČEK. Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. Online. In Isil Dillig, Serdar Tasiran. CAV 2019: Computer Aided Verification. Cham (Switzerland): Springer, 2019, s. 64-73. ISBN 978-3-030-25542-8. Dostupné z: https://doi.org/10.1007/978-3-030-25543-5_4.
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.