STORM: static unit checking of concurrent programs

Concurrency is inherent in today´s software. Unexpected interactions between concurrently executing threads often cause subtle bugs in concurrent programs. Such bugs are hard to discover using traditional testing techniques since they require executing a program on a particular unit test (i.e. input) through a particular thread interleaving. A promising solution to this problem is static program analysis since it can simultaneously check a concurrent program on all inputs as well as through all possible thread interleavings. This paper describes a scalable, automatic, and precise approach to static unit checking of concurrent programs implemented in a tool called Storm. Storm has been applied on a number of real-world Windows device drivers, and the tool found a previously undiscovered concurrency bug in a driver from Microsoft´s Driver Development Kit.