Precise and Automated Symbolic Analysis of Concurrent Programs

Опубликовано 17 августа 2016, 21:06

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.