Starting date: immediately

Context Software transformations occur very frequently in practice. Such transformations are done for various purposes though manual refactoring or automatic transformations. However, in this thesis we focus on transformations that must preserve the functional behavior of the software that is being transformed. For instance, software transformations applied by compiler optimizations or obfuscation transformations must preserve the functional behavior of the software, i.e. the original and the transformed counterpart must yield the same output when given the same input. Symbolic execution has been proposed as a technique which could be used to find whether 2 programs have the same functional behavior [1, 2, 3]. Since it is assumed that symbolic execution can explore a large part of the execution tree of a program, it can also find an input for which the output of the original and transformed programs differs. However, in practice there are many limitations to this approach [4, 5]. In this thesis we intend to uncover the impact these limitations have on equivalence testing. Goa