Disertační práce
Získaná ocenění: Ocenění děkana FI za vynikající disertační práci Cena rektora za vynikající disertační práci

Satisfiability of Quantified Bit-Vector Formulas: Theory and Practice

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

Množství současných aplikací, od bioinformatiky, přes rozvrhování, až po analýzu software a hardware, spoléhá na schopnost rozhodnout splnitelnost zadané logické formule v zadané logické teorii. Tento rozhodovací problém je znám pod názvem Satisfiability Modulo Theories (SMT). Tato disertační práce se soustředí na jednu konkrétní teorii, která je podstatná pro analýzu software a hardware: teorii bitových …více

Abstract

Multiple modern applications, ranging from bioinformatics, through job scheduling, to software and hardware analysis rely on ability to decide satisfiability of a given formula in a given logical theory. This decision problem is called satisfiability modulo theories (SMT). This thesis focuses on one particular theory, which is of paramount importance in analysis of software and hardware: the theory …více

Klíčová slova
satisfiability satisfiability modulo theories bit-vectors complexity logic
Administrativní informace
Práce zkontrolována:
1. 6. 2019 10:43, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
1,2 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
18. 9. 2019
Práce byla úspěšně obhájena

Vedoucí

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

Oponenti

Prof. Cesare Tinelli
The University of Iowa
Univ.-Prof. Dr. Armin Biere
Johannes Kepler University, Linz
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika (čtyřleté)
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.