Precise and Automated Symbolic Analysis of Concurrent Programs
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.
Speaker Details
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.
- Date:
- Speakers:
- Zvonimir Rakamaric
- Affiliation:
- University of British Columbia
-
-
Jeff Running
-
