Concurrency can be used to make software implementations more responsive. However, concurrency also makes program analyses much more difficult and can introduce bugs which can cause two executions with the same inputs to give different outputs. Symbolic Execution has shown that it can be used to analyse a program and detect bugs deep in the code which can only be reached with specific inputs. However, this has been done mostly on sequential programs, not concurrent ones.

We explore how to leverage the strengths of symbolic execution to determine if a program contains data-races. This is accomplished through transforming an input program into a control flow graph, which contains information of all possible assignments in concurrent threads. By using this design, the symbolic execution generates some invalid models as it is an over approximation, and thus given that exact model, it is not always possible to verify if the detected data-race is a false positive or not.

The thesis thus also discusses how this can be improved, and presents an improvement for the symbolic execution, which has shown to be quite effective for concurrent programs with two threads. For concurrent portions of code, the discussion also mentions potential mitigations and extensions which can help improving the symbolic execution to a point, where a concrete execution should not be necessary to verify that the detected data-race can indeed occur.