Bakalářská práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

Caching SMT Queries in SymDivine

Jan Mrázek
Anotace

Škálovatelnost nástrojů pro automatickou verifikaci softwaru je klíčový faktor pro použitelnost těchto nástrojů. Existuje mnoho způsobů, jak ji vylepšit. Obětování paměťové náročnosti za účelem ušetření času je jeden z možných přístupů, zejména pokud je procedura založena na rozhodování splnitelnosti logických formulí. Cacheování nekvantifikovaných SMT formulí je běžně používáno v symbolické exekuci …více

Abstract

Scalability of automatic verification tools is a crucial factor for usability of such tools in practise. There are vast number of ways to improve it. Trading off space for time is one of a classic approaches to improving time efficiency of these tools, mainly used when constraints satisfiability checking plays a central role. Caching of quantifier-free Satisfiability Modulo Theories (SMT) queries is …více

Klíčová slova
Formal Verification C C++ LLVM Model Checking SMT Caching Implementaion
Zadání práce
The goal of the thesis is to develop and evaluate a caching mechanism for SMT queries in the context of semi-symbolic verification of multithreaded C and C++ programs. The student is expected to implement the newly developed method and evaluate its practical efficiency within the SymDIVINE verification tool on an appropriate set of C/C++ programs.
Administrativní informace
Práce zkontrolována:
25. 5. 2016 10:31, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
718,3 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
23. 6. 2016
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Oponent

RNDr. Martin Jonáš, Ph.D., učo 359542
KTP 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.