Precise and Automated Symbolic Analysis of Concurrent Programs

Date

April 14, 2010

Speaker

Zvonimir Rakamaric

Affiliation

University of British Columbia

Overview

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.

Speakers

Zvonimir Rakamaric

Zvonimir Rakamaric is a Ph.D. Candidate at the University of British Columbia. His research is focused on improving software correctness and reliability by developing automated software analysis and verification techniques and tools. Zvonimir’s M.Sc. thesis was on verification of heap-manipulating programs, and currently he is mainly working on an automatic, precise, and scalable checker for concurrent systems code. Zvonimir holds a M.Sc. degree in computer science from the University of British Columbia and a Dipl.Ing. degree in computer science from the Faculty of Electrical Engineering and Computing at the University of Zagreb. For more information about Zvonimir, visit www.zvonimir.info.