The goal of the thesis is to design and implement an algorithm that gets an LLVM program with distinguished error locations and produces an LLVM program that starts its execution in the error locations of the original program and encodes all the possible paths against the control flow of the original program. The produced reversed program will have a feasible path to its error location if and only if the original program has a feasible error path.

The production of reversed programs is motivated by the fact that some program verification techniques search a given program from its initial location, and thus they cannot quickly decide that a given program is correct if the reason for the unreachability of error locations is near these locations. Such techniques can be more efficient on reversed programs of this kind.

The thesis will also experimentally evaluate the efficiency of the program verifier Symbiotic on reversed programs from SV-COMP 2025.