Symbiotic je open-source nástroj pro verifikaci programů,
který využívá prořezávání programů ke zrychlení verifikace.
Tato práce popisuje implementaci nového přořezávacího algoritmu
založeného na grafech závislostí, který nahrazuje starý
algoritmus,
jenž používá data-flow přístup. V první části práce dáme
čtenáři nahlédnout
do základů teorie přořezávání programů a popíšeme prořezávací
algoritmy.
Poté popíšeme algoritmy nutné pro výstavbu grafu závislostí a
jejich
implementaci. Tyto jsou jmenovitě: algoritmus pro výpočet
kontrolních závislostí,
analýza ukazatelů a analýza dosažitelných definic. Na konci
práce porovnáváme
starý a nový prořezávací algoritmus na netriviální množině dat.