Open-source verification tool Symbiotic uses program slicing to decrease the analysis running time. The goal of this thesis is to implement a slicing algorithm based on dependence graphs, that will be faster and more precise over the current implementation following the Weiser's algorithm. The implementation is expected to work on widely used compiler infrastructure LLVM, thus to be generic enough to be deployed even outside of the Symbiotic. The text report will describe the theory of program slicing as well as the implementation part and connected problems. Student will also experimentally evaluate the implemented algorithm on a set of non-trivial benchmarks.