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

Symbolic Model Checking via Program Transformations

Bc. Henrich Lauko, učo 410438
Anotace

K zabepečeniu spoľahlivosti softvéru sa bežne využíva testovanie a statická analýza. Ak máme dokázať korektnosť programu, je ale nutné preveriť všetky jeho možné behy. K tomuto účelu sú využívané formálne verifikačné metódy, ktoré tento proces automatizujú. Verifikáciu ale komplikujú vstupy, ktoré spôsobujú veľký nárast možných behov. V tejto práci predstavujeme techniku, ktorá umožňuje verifikačným …více

Abstract

To show reliability of software, developers usually reach out for testing and static analysis. However, to prove correctness, all behaviours of a program need to be checked. In this respect, formal verification methods aim to provide an automated approach to verification. A big obstacle are inputs because they massively increase the number of behaviours of the program. In this thesis, we present a …více

Klíčová slova
formal verification model checking symbolic model checking DIVINE abstraction LLVM implementation program transformation LART C C++
Zadání práce
Cílem práce je navrhnout a implementovat programové transformace, na úrovni LLVM bitkódu, které umožní, resp. usnadní, další analýzu. Jedná se zejména o implementaci automatické abstrakce hodnot proměnných (převod hodnot a operací z domény konkrétních čísel do domény symbolické manipulace s výrazy). Implementace transformací by měla být provedena v rámci nástroje LART (který je součástí balíku DIVINE). Pro účely vyhodnocení použitelnosti navržených transformací student svoji implementaci napojí na prototypovou implementaci symbolického prohledávání stavového prostoru, která v nástroji DIVINE existuje a využívá ke srovnání symbolických hodnot externí SMT solver.
Administrativní informace
Práce zkontrolována:
14. 12. 2017 09:24, RNDr. Petr Ročkai, Ph.D., učo 139761
Plný text práce
515,8 KB / soubor PDF
Přílohy (3)
Jazyk práce
angličtina angličtina
Termín obhajoby
1. 2. 2018
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

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

Literatura

  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
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.