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

LLVM Transformations for Model Checking

LLVM Transformations for Model Checking

Bc. Vladimír Štill, učo 373979
Anotace

Tato práce je zaměřená na využití LLVM transformací jako kroku, který je předřazen verifikaci programů v programovacích jazycích C a C++ s pomocí nástroje pro explicitní model checking DIVINE. Práce demonstruje, že LLVM transformace mohou být použity jak pro rozšíření schopností verifikačního nástroje, tak i pro redukci velikosti stavového prostoru. Co se rozšíření schopností verifikačního nástroje …více

Abstract

This work focuses on application of LLVM transformations as a preprocessing step for verification of real-world C and C++ programs using the explicit-state model checker DIVINE. We demonstrate that LLVM transformations can be used for extension of verifier capabilities and for reduction of the state space size. In the case of extension of verifier capabitilies, the main focus is on verification under …více

Klíčová slova
Formal Verification C C++ LLVM Model Checking Parallel DIVINE LART LLVM Transformation Weak Memory Models Total Store Order Implementation
Zadání práce
When model checking a C++ program with an explicit-state model checker DIVINE, the input program is first translated to an LLVM bitcode that serves as an input formalism for the model checker. The goal of this thesis is to explore possibilities of LLVM bitcode to LLVM bitcode transformations that could either improve or extend capabilities of the model checker. It is expected that within the thesis couple of tranformations will be suggested, implemented and their impact on the process of verification evaluated.
Administrativní informace
Práce zkontrolována:
13. 1. 2016 08:02, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
506,3 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
15. 2. 2016
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

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