Original title: Sumarizace větvených cyklů
Translated title: Branching loop summarization
Authors: Tatarko, William ; Blicha, Martin (advisor) ; Bednárek, David (referee)
Document type: Master’s theses
Year: 2021
Language: eng
Abstract: [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. 1 V 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
Keywords: summarization|algorithm|reachabilitiy|verification|digraphs; sumarizace|algoritmus|dosažitelnost|verifikace|orientované grafy

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/127784

Permalink: http://www.nusl.cz/ntk/nusl-448637


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Master’s theses