Bakalářská práce

Improvements of reaching definitions analysis in Symbiotic

Tomáš Jašek
Anotace

Cieľom práce je zrýchliť analýzu dosažitelných definícií, ktorá je súčasťou verifikačného nástroja Symbiotic. Originálna, "hustá" analýza propaguje všetky dosažitelné definície naprieč celým grafom toku riadenia programu. Nová analýza je založená na transformácii operácií s pamäťou do SSA formy, z ktorej sa dosažiteľné definície dajú priamo vyčítať. Experimenty ukazujú, že nová implementácia je pomalšia …více

Abstract

The aim of this thesis is to improve the speed of the reaching definitions analysis that is part of software verification tool Symbiotic. The original “dense” analysis propagates all reaching definitions throughout the whole control flow graph of a program. The new analysis is based on transformation of memory operations in a program to static single assignment form, which directly reveals reaching …více

Klíčová slova
C++ formal methods Formela implementation static analysis Symbiotic
Zadání práce
Cílem práce je zrychlit analýzu dosažitelných definic v nástroji Symbiotic. Student se seznámí s moderními technikami počítání dosažitelných definic a stručně je popíše. Jedna z technik bude popsána detailněji a implementována do nástroje Symbiotic. Součástí práce bude experimentální porovnání nové a staré implementace analýzy dosažitelných definic na netriviální sadě benchmárků, například ze soutěže SV-COMP.
Administrativní informace
Práce zkontrolována:
28. 5. 2018 19:58, RNDr. Marek Chalupa, Ph.D.
Jazyk práce
angličtina angličtina
Termín obhajoby
27. 6. 2018
Práce byla úspěšně obhájena

Vedoucí

RNDr. Marek Chalupa, Ph.D.
KTP FI MU

Oponent

RNDr. Petr Ročkai, Ph.D., učo 139761
KPSK FI MU

Konzultant

prof. RNDr. Jan Strejček, Ph.D., učo 3366
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.