Symbiotic is a tool that can inspect memory safety of given C programs. In the current state, it may have some performance issues when deciding the memory safety of accesses into arrays that are done inside a loop. However, many of such accesses are easy to qualify as safe when one identifies the control variables of the loop, the way these variables change, and relations between the control variables and other values in the program.

The goal of this thesis is to design and implement a solution for qualifying (some) array accesses inside loops as safe or unsafe. More precisely, the student will design and implement an analysis of relations between values in a program and use this analysis to mark memory accesses into an array via a control variable as valid or possibly out of bounds and thus improve the analysis of memory safety in Symbiotic.

Apart from the implementation, the student is expected to evaluate her/his solution on a non-trivial set of benchmarks and analyze the results, namely the impact of the improvements on the capabilities of Symbiotic.