Rigorózní práce

Abstractions via Program Transformations

Mgr. Henrich Lauko, učo 410438
Anotace

Při automatické verifikaci programů využívá většina nástrojů abstrakce ke snížení složitosti analyzovaných systémů. Přestože jsou tyto techniky široce používány, je jejich implementace obvykle pevně spjata s konkrétními nástroji, což způsobuje nežádoucí složitost implementace a znemožňuje jakékoli použití v jiných nástrojích. Ve svém výzkumu se zaměřuji na zkoumání technik založených na abstrakci …více

Abstract

In computer-aided verification, most of the tools leverage abstraction techniques to reduce the complexity of analyzed systems. Even though these techniques are widely adopted, they are usually tightly integrated into tools, causing undesired complexity, and neglect any reusable design. In my research, I focus on the investigation of abstraction-based techniques used in program verification as abstract …více

Klíčová slova
formal verification model checking symbolic model checking divine abstraction llvm implementation program transformation lart C C++
Administrativní informace
Práce zkontrolována:
27. 11. 2019 14:56, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
1,6 MB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
14. 1. 2020
Práce byla úspěšně obhájena

Oponenti

prof. RNDr. Luboš Brim, CSc.
KTP FI MU
doc. Mgr. Adam Rogalewicz, Ph.D.
abs FI MU, FIT VUT v Brně
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Teoretická informatika

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.