Events Calendar

CS Colloquium: Chao Wang (Virginia Tech) - Symbolic Analysis for Detecting and Mitigating Errors in Concurrent Software

Speaker: Chao Wang, Virginia Tech

Talk Title: Symbolic Analysis for Detecting and Mitigating Errors in Concurrent Software

Series: CS Colloquium

Abstract: This lecture satisfies requirements for CSCI 591: Computer Science Research Colloquium

The use of multi-core architecture is now pervasive, spanning from embedded systems and smart phones, to commodity PCs, all the way to high-end servers and distributed systems. As such, developers must write concurrent software. However, writing correct and efficient concurrent software is difficult. Although automated analysis to aid in their development would be invaluable, existing methods are either fast but inaccurate, or accurate but slow, due to the inherent difficulty in circumventing the path and interleaving explosion problem. In this talk, I will introduce a series of symbolic predictive analysis methods for analyzing concurrent software. This analysis consists of two steps. First, we derive a predictive model from the execution traces collected at run time as well as the software code. The model captures not only the given executions but also the alterative interleavings of events in these executions. Then, we use symbolic analysis to check if errors exist in these alternative interleavings. This is accomplished by capturing these interleavings and the error conditions using a set of logic formulas and deciding them using a Satisfiability Modulo Theory (SMT) solver. Although our primary focus is to reduce the cost associated with analyzing and verifying concurrent software, the predictive model and related analysis techniques are also useful in addressing issues related to performance and security.

Biography: Chao Wang is an Assistant Professor of the ECE Department and the CS Department (by courtesy) of Virginia Tech. He received the ONR Young Investigator award in 2013 and the NSF CAREER award in 2012. His area of specialization is Software Engineering and Formal Methods, with emphasis on concurrency, formal verification, and program synthesis. He published a book and more than fifty papers in top venues of related field including ICSE, FSE, ASE, ISSTA, CAV, PLDI, and POPL. He received the FMCAD Best Paper award in 2013, the ACM SIGSOFT Distinguished Paper award in 2010, the ACM TODAES Best Paper of the Year award in 2008, and the ACM SIGDA Outstanding PhD Dissertation award in 2004. Dr. Wang received his PhD degree from the University of Colorado at Boulder in 2004. From 2004 to 2011, he was a Research Staff Member at NEC Laboratories of America in Princeton, NJ, where he received a Technology Commercialization award in 2006.

Host: CS Department

Location: Olin Hall of Engineering (OHE) - 136

Audiences: Everyone Is Invited

Contact: Assistant to CS chair