Cílem práce je navrhnout algoritmus pro automatické hledání chyb ve fragmentech programů (funkcích, překladových jednotkách, knihovnách). Protože není k dispozici kompletní program, který by bylo lze spustit, jedná se o formu statické analýzy. Algoritmus by měl být nicméně postaven nad existující rozhodovací procedurou pro hledání chyb, resp. dokazování jejich absence, v kompletních programech. Protože vstupem této procedury je kompletní spustitelný program, tato může využívat technik přesnější dynamické analýzy. Navrhovaný algoritmus by tedy měl vstupní fragment programu vhodně doplnit na kompletní program tak, aby chyby ve vstupním fragmentu odpovídaly chybám ve výstupním programu. Z povahy věci je zřejmé, že ne každá chyba v doplněném programu odpovídá skutečné chybě ve vstupním fragmentu: navrhovaný algoritmus by měl nicméně množství takovýchto „falešných“ chyb minimalizovat. Součástí algoritmu by měl být výpočet (podle možnosti nejslabších možných) vstupních podmínek relevantních celků vstupního fragmentu. Součástí práce je prototypová implementace postavená na mezireprezentaci LLVM a dynamické analýze poskytované nástrojem DIVINE. Očekává se, že prototyp bude schopen zpracovat programy, které pracují s celočíselnými skaláry. Podpora práce s pamětí nechť je volitelným rozšířením.