Submitted: March 2016
Abstract
Software reliability and verification are of growing importance. As concurrent programming got attention only recently, there is a lot of interest and active research.
Within the topic of concurrent programming, especially Data Races are a common source of errors. Ranging from operating system kernels and real-time systems to applications for mobile devices, Data Races may occur anywhere. Often they are very hard to track down since they cause unexpected program behavior which may even not be directly observable.
Thus developing techniques to find Data Races reliably is highly desirable. Unfortunately, Data Race Detection, as well as general verification, is undecidable in general. So the problem must be relaxed to achieve at least a partial solution.
In this thesis, a concurrent programming language called pseuCo is utilized to develop a technique that finds Data Races automatically by means of static program analysis. pseuCo represents a sensible relaxation as it does not support aliasing (which by itself is not decidable). This allows for a partial solution of the problem.
The implementation of the technique is embedded in a larger piece of software called the “pseuCo-Verification-Toolset”. It attempts to provide a common platform based on pseuCo that is very easy to expand and to reason about. Hence, it may be used to explore and implement solutions for other verification problems related to concurrency.