Master's thesis
Awards: Dean's Award for an Outstanding Final Thesis

LLVM Transformations for Model Checking

LLVM Transformations for Model Checking

Bc. Vladimír Štill, UČO 373979
Abstract

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 …more

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 …more

Keywords
Formal Verification C C++ LLVM Model Checking Parallel DIVINE LART LLVM Transformation Weak Memory Models Total Store Order Implementation
Thesis description
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.
Administrative information
The thesis has been checked:
13/1/2016 08:02, prof. RNDr. Jiří Barnat, Ph.D., UČO 3496
Full text of thesis
506,3 KB / file PDF
Attachments (1)
Language used
English English
Defence date
15/2/2016
The thesis was defended successfully

Supervisor

prof. RNDr. Jiří Barnat, Ph.D., UČO 3496
KTP FI MU

Reader

prof. RNDr. Jan Strejček, Ph.D., UČO 3366
ITI FI MU
Cite this text
Masaryk University Faculty of Informatics
Programme
Informatics
Field of Study

Theses on a related topic

List of theses with an identical keyword.

Similar documents

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