Disertační práce

Abstraction via Program Transformation

RNDr. Henrich Lauko, učo 410438
Anotace

V oblasti autonomní verifikace programů jsou abstrakční techniky nezbytné, protože hrají kritickou roli při snižování složitosti verifikačního procesu na zvládnutelné velikosti. Tyto techniky jsou však obvykle pevně integrovány do nástrojů, což vede k nežádoucí složitosti a opomenutí opakovaně použitelného návrhu. Pokud chce někdo použít konkrétní abstrakci v několika nástrojích, běžným přístupem je …více

Abstract

In the field of computer-aided verification, abstraction techniques are indispensable as they play a critical role in reducing the complexity of the verification process to manageable sizes. However, these techniques are usually tightly integrated into tools, resulting in undesired complexity and neglect of reusable design. If one wants to employ a particular abstraction in several tools, the common …více

Klíčová slova
program analysis software verification model checking symbolic model checking abstract execution divine llvm program transformation compilation abstraction refinement heap analysis string analysis lart C C++ implementation
Administrativní informace
Práce zkontrolována:
21. 11. 2023 11:13, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
1,9 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
20. 2. 2024
Práce byla úspěšně obhájena

Vedoucí

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

Oponenti

Prof. Dr. Gidon Ernst
LMU Munich
prof. Ing. Tomáš Vojnar, Ph.D., učo 134390
KPSK FI MU, FIT VUT v Brně

Konzultant

RNDr. Petr Ročkai, Ph.D., učo 139761
KPSK FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Technologie a metodologie počítačových systémů

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.