Rigorózní práce

SMT Solving for the Theory of Bit-Vectors

Mgr. Martin Jonáš, učo 359542
Anotace

Teze mé dizertační práce se zabývají rozhodováním splnitelnosti formulí logiky prvního řádu nad teorií bitových vektorů. Teze nejprve popisují současně používané přístupy k řešení splnitelnosti formulí výrokové logiky a prvořádových formulí nad danou teorií. Poté se věnují postupům používaným konkrétně při řešení splnitelnosti formulí nad teorií bitových vektorů, a to jak formulí bez kvantifikátorů …více

Abstract

My PhD thesis proposal is dedicated to the problem of deciding satisfiability of first-order formulas in the theory of bit-vectors. First, state-of-the-art approaches to solving satisfiability of propositional formulas and to solving satisfiability modulo theories are described. Subsequentially, approaches to solving satisfiability of both quantifier-free and quantified formulas over the theory of …více

Klíčová slova
satisfiability satisfiability modulo theories bit-vectors quantifiers quantifier instantiation binary decision diagrams dpll cdcl
Administrativní informace
Práce zkontrolována:
28. 9. 2016 01:25, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
1,2 MB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
12. 1. 2017
Práce byla úspěšně obhájena

Oponenti

doc. RNDr. Jan Kofroň, Ph.D.
MFF UK v Praze
prof. Ing. Tomáš Vojnar, Ph.D., učo 134390
KPSK FI MU, FIT VUT v Brně
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.