Symbolic Predictive Analysis for Improving the Reliability and Security of Concurrent Software

ABSTRACT

Multi-core and multi-processor systems are becoming increasingly popular. However, our ability to effectively harness their computing power is predicated upon advances in tools and algorithms for analyzing and verifying concurrent programs. Concurrent programs are notoriously difficult to write, and a key reason for this is the behavioral complexity resulting from the large number of interleavings of concurrent components. In this talk, I will introduce a symbolic predictive analysis for runtime detection of concurrency errors, by monitoring and subsequently analyzing the execution traces of a program. This analysis consists of two steps: First, we derive a predictive model using the trace information collected at run time as well as the program source code. What this model captures are not just the given traces, but all possible interleavings of events of these traces. Then, we use symbolic reasoning to check whether there are concurrency errors in any of these interleavings. Although the primary focus is to increase the reliability of the concurrent systems, this predictive model and the related analysis techniques are also useful in addressing issues related to performance and security. BIO Dr. Chao Wang is an Assistant Professor in the ECE department at Virginia Tech (USA). His research is in the areas of formal verification, software verification, and program analysis. He received the ONR YIP Award from the Office of Naval Research in 2013, and the NSF CAREER Award from the National Science Foundation in 2012 -- both are prestigious awards for early-career faculty members. He has published a book and more than 50 peer-reviewed papers, many of which appeared in flagship conferences and journals in his field. He received the ACM SIGSOFT Distinguished Paper Award in 2010, the Best Journal Paper of the Year Award from the ACM Transactions on Design Automation of Electronic Systems in 2008, and the ACM SIGDA Outstanding Ph.D. Dissertation Award in 2004. Before joining the faculty of Virginia Tech in 2011, he was research staff member in NEC Laboratories for seven year, where he developed many in-house software analysis and verification tools. He received an NEC Labs Technology Commercialization Award in 2006.