The tool Symbiotic uses its own fork of symbolic executor KLEE. This fork has been extended to be able to perform symbolic-size memory allocations. However, the memory model in this fork of KLEE still suffers from using addresses returned from the host system as identifiers of internal objects. That leads to crashes when analyzing 32-bit programs on 64-bit systems and the inability to soundly compare pointers. The student will get rid of using the host system addresses as identifiers of internal objects in KLEE and implement on-demand memory allocation in the cases where there is a need to allocate memory on the host system (e.g. when calling an external function).