Static code analysis in multi-threaded environments

In this work we follow an intermediate approach that tries to use sound and conservative static code analysis techniques to avoid certain classes of bugs without having to conduct a full blown formal proof of correctness. The methods developed in this work are tailored to concurrent systems where global data is shared between all threads. While this requirement is not strictly necessary for the soundness of the analysis we shall see that it greatly increases the accuracy. In this context accuracy refers to the likelihood that a problem reported by the analysis is caused by an actual bug in the software and not by an inadequacy of the analysis methods. The usefulness of the methods presented will be supported by several case studies conducted on real life software systems of significant size