Multithreaded programming is hard, and programmer errors can lead to unintentional data races. Bugs that stem from data races are notoriously subtle and difficult to detect, as they tend to rely on rare thread schedules that are unlikely to occur on a non-deterministic scheduler. Furthermore, a bug may require other rare conditions in order to manifest, such as certain file inputs and system call responses. Exploring all such possibilities leads to state-space explosion for large multithreaded programs.

My research involves scalable data-dependent data race detection using symbolic execution. It is important that real programs can be analysed, even those that interact with the environment (e.g. programs that read files and behave differently depending on the contents). The use of symbolic execution allows a large range of inputs to be considered, including file inputs and other sources of non-determinism. An important aspect is developing reductions that reduce the number of interleavings that need to be explored and heuristics that drive the search towards data races. Heuristics are particularly interesting, as they can use information that is gained statically and/or dynamically to prioritise the exploration of paths that are more likely to lead to data races.