Název:
Sumarizace větvených cyklů
Překlad názvu:
Branching loop summarization
Autoři:
Tatarko, William ; Blicha, Martin (vedoucí práce) ; Bednárek, David (oponent) Typ dokumentu: Diplomové práce
Rok:
2021
Jazyk:
eng
Abstrakt: [eng][cze] In this thesis we present a novel algorithm for summarization of loops with multiple branches operating over integers. The algorithm is based on anal- ysis of a so-called state diagram, which reflects feasibility of various branch interleavings. Summarization can be used to replace loops with equivalent non-iterative statements. This supports examination of reachability and can be used for software verification. For instance, summarization may also be used for (compiler) optimizations. 1V této práci představujeme nový algoritmus na sumarizaci cyklů s více větvemi pracujícími s celými čísly. Algoritmus je založen na analýze tzv. stavového diagramu, který zachycuje možné přechody mezi větvemi. Suma- rizace může být použita na nahrazení cyklů ekvivalentními neiterativními příkazy. Toto umožňuje analýzu dosažitelnosti a může být použito na veri- fikaci softwaru. Sumarizace může být také například použita na optimalizace (kompilátorů). 1
Klíčová slova:
sumarizace|algoritmus|dosažitelnost|verifikace|orientované grafy; summarization|algorithm|reachabilitiy|verification|digraphs