Diplomová práce

Rozšíření nástroje pro symbolickou exekuci KLEE

Extension of the KLEE symbolic analysis tool

Bc. Peter Hruška, učo 208315
Anotace

Táto práca sa zaoberá rozšírením nástroja pre symbolickú exekúciu KLEE o funkcionalitu nahradzovania symbolických výrazov reálnymi hodnotami, ktorá je prítomná v nástroji DART. Zameriava sa hlavne na analýzu fungovania KLEE, možnosti realizácie úpravy, samotnou implementáciu zmeny v KLEE a odskúšanie modifikovanej verzie KLEE na reálnych programoch oproti originálnej verzii.

Abstract

This text deals with extension of a tool for symbolic execution named KLEE by functionality of substitution of symbolic expressions with concrete values which is present in tool named DART. It is focused mainly on analysis of KLEE's working, options of modifications realisation, implementation of change in KLEE itself and tesing of the changed version of KLEE on real programs agains the original version.

Zadání práce
Symbolická exekuce je v poslední době stále populárnější technika pro automatické hledání chyb programech. Na této technice je založeno několik softwarových nástrojů - například EXE, KLEE, DART nebo SAGE. Cílem diplomové práce je rozšířit volně dostupný nástroj KLEE o techniku tzv. "directed automated random testing", která byla poprvé navrhnuta v nástroji DART. V ideálním případě by práce měla obsahovat i srovnání chování rozšířeného a původního KLEE na konkrétních programech.

Literatura:

  • Klee: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. Cristian Cadar, Daniel Dunbar, Dawson Engler: Operating System Design and Implementation (OSDI), Dec, 2008
  • DART: Directed Automated Random Testing (Patrice Godefroid and Nils Klarlund and Koushik Sen) Proceedings of PLDI'2005 (ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation), pages 213-223, Chicago, June 2005.
Práce zkontrolována:
9. 1. 2013 09:50, doc. Mgr. Jan Obdržálek, PhD., učo 1552
Jazyk práce
slovenština slovenština
Termín obhajoby
8. 2. 2013
Práce byla úspěšně obhájena

Vedoucí

doc. Mgr. Jan Obdržálek, PhD., učo 1552
ITI FI MU

Oponent

Mgr. Jiří Slabý, Ph.D.
abs FI MU

Konzultant

Mgr. Marek Trtík, Ph.D., učo 329313
KPSK FI MU

  • 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.