Disertační práce
Získaná ocenění: Ocenění děkana FI za vynikající disertační práci Cena rektora za vynikající disertační práci

Program Slicing and Symbolic Execution for Verification

RNDr. Marek Chalupa
Anotace

Existuje mnoho formálních metod k dokazování či vyvracení vlastností programů (např. že žádný příkaz assert nemůže být porušen). Jedna taková metoda je symbolická exekuce, která systematicky vyčísluje možné běhy v programu. Tento přístup musí dříve či později nevyhnutelně selhat kvůli nedostatečným zdrojům (např. čas nebo paměť), pokud je počet cest v analyzovaném program velký. Tomuto problému se …více

Abstract

There are many formal methods for proving or disproving various properties of programs (e.g., that all assertions in a program hold). One such method is symbolic execution that systematically enumerates feasible execution paths of a program. This approach must inevitably fail due to insufficient resources (e.g., time or memory) if the number of execution paths in a program is huge. This is the so-called …více

Klíčová slova
program slicing data dependence control dependence symbolic execution backward symbolic execution k-induction invariants
Administrativní informace
Práce zkontrolována:
9. 10. 2021 02:21, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
2,9 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
12. 4. 2022
Práce byla úspěšně obhájena

Vedoucí

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

Oponenti

Dr. rer. nat. Dirk Beyer
LMU Munich
Prof. Corina Pasareanu
Carnegie Mellon University
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Fundamenty informatiky

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.