Real-world software is undergoing paradigm shifts, and these shifts introduce reliability and security challenges. One paradigm shift is that software is moving from single-threading to multi-threading. However, multi-threading is notoriously hard to get right, and a key reason is that software may run into too many possible thread interleavings, which aggravates understanding, testing, analysis, and can lead to wrong outputs and security breaches. Another paradigm shift is that software has become larger and more complicated, while still having to obey critical rules (e.g., allocated memory must be freed, and assertions must always succeed), as violating these rules can cause resource leaks and program crashes. Unfortunately, existing techniques can not feasibly check these rules on real-world software due to path explosion. 

In this talk, I will address the above challenges with two new techniques. First, I will present Stable Multi-Threading (StableMT), a reliable and secure parallism paradigm that can greatly reduce the amount of thread interleavings, and a practical StableMT runtime system that is fast and scalable with a wide range of popular software. Second, I will introduce rule-directed pruning, a new algorithm that can soundly prune program paths without missing violations of a checked rule, leading to exponential speedup of a state-of-the-art checking tool, and numerous new security violations confirmed or fixed in widely used software. These two new techniques have good potential to benefit many other reliability and security techniques.

Heming Cui is a PhD candidate at Computer Science of Columbia University. His thesis research is focused on improving software reliability and security with runtime and program analysis techniques. His general interests are in operating systems, programming languages, and distributed systems. Before joining Columbia, he obtained his master and bachelor degrees from Tsinghua University, Beijing, China.