Bakalářská práce

Constructing Alignment Automata for Equivalence Checking of Programs

Andrea Zimovčáková
Anotace

Overovanie ekvivalencie programov je kľúčovou úlohou v oblasti verifikácie softvéru, optimalizácie kompilátorov a validácie prekladu. Používa sa na zabezpečenie rovnakého pozorovateľného správania dvoch programov. Nedávne techniky konštruujú automaty zarovnania programov (z anglického Program Alignment Automata, PAA) na porovnávanie správania riadiaceho toku a dokazovanie ekvivalencie aj pri zložitých …více

Abstract

Program equivalence checking is an essential task in software verification, compiler optimization, and translation validation, where it is used to ensure that two programs exhibit the same observable behavior. Recent alignment-based techniques construct Program Alignment Automata (PAA) to compare control-flow behaviors and prove equivalence even under complex compiler optimizations. However, existing …více

Klíčová slova
Program Equivalence Checking Symbolic Execution Program Alignment Automata (PAA) Trace-Free Verification Software Verification
Zadání práce
Checking whether two programs are equivalent has a number of applications and there exist various approaches to the problem. The first goal of the thesis is to implement the automata-theoretic procedure described in the paper "Direct Construction of Program Alignment Automata for Equivalence Checking". The second goal is then to apply the procedure to programs and to experimentally evaluate its effectiveness and efficiency.
Administrativní informace
Práce zkontrolována:
23. 1. 2026 14:17, prof. Dr. rer. nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D., učo 139914
Plný text práce
821,5 KB / soubor PDF
Přílohy (2)
Jazyk práce
angličtina angličtina
Termín obhajoby
5. 2. 2026
Práce byla úspěšně obhájena

Vedoucí

prof. Dr. rer. nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D., učo 139914
KTP FI MU

Oponent

Mgr. Marek Trtík, Ph.D., učo 329313
KPSK FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
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.