Precise and Automated Symbolic Analysis of Concurrent Programs

Speaker  Zvonimir Rakamaric

Host  Shaz Qadeer

Affiliation  University of British Columbia

Duration  01:06:26

Date recorded  14 April 2010

Software is large, complex, and error-prone. The trend of switching to parallel and distributed computing platforms (e.g. multi-cores, cloud computing) makes software development even more complex (e.g. Heisenbugs). In this talk, I'll present my research towards improving the reliability of concurrent programs by building a scalable tool for precise and automated static analysis of concurrent executions. In the first part of the talk I will introduce STORM, a static assertion checker for concurrent software components: I'll present algorithms and techniques used in the tool, as well as the latest results of applying STORM on drivers in the Win8 source depot. In the second part I'll focus on future plans and promising research directions for STORM as a platform for precise symbolic reasoning of concurrent executions.

©2010 Microsoft Corporation. All rights reserved.
> Precise and Automated Symbolic Analysis of Concurrent Programs