Symbolic Execution is a technique in software testing which analyses a given program automatically. To do so the program’s (or function’s) inputs are represented as symbolic values and test cases to cover all different possible combinations are generated automatically. By these means, a completely and successfully tested piece of code either detects errors for some specific input that then can be used for further debugging or no errors and is therefore proven to be correct according the executed assertions. The last part makes Symbolic Execution also interesting for software verification. Although this is only in theory of real interest, since analysing all different possible paths of a program is really hard to achieve in practice. Most of the time it actually is even near impossible with today’s technology in any feasible amount of time. This problem is due to the fact that Symbolic Execution tries every possible path of a given software to test it completely and the amount of paths in a program typically grows exponentially, which is often also denoted as path explosion problem. For practical usage this therefore represents a huge problem when thinking about scalability.
With these problems of an otherwise great process in mind, one can see that the task of finding a good execution sequence is crucial for the practical use of this method. One possible approach that will be followed in this thesis is to build or modify the searcher in such a way to improve the choice of paths to take along the program and therefore have a higher chance of finding an error early on.