As software becomes increasingly pervasive and complex, masses of users are exposed to unintended software failures and deliberate cyber-attacks. Program analysis is a widely adopted technology to enforce software quality. Existing program analyses are expressed in the form of logical rules that are handcrafted by experts. While this logic-based approach has many benefits, however, it cannot handle uncertainty and lacks the ability to learn and adapt. This in turn hinders the accuracy, scalability, and usability of program analysis tools in practice.
I will present a methodology and framework to incorporate probabilistic reasoning into existing program analyses that are based on logical reasoning. The framework comprises a front-end, which automatically integrates probabilities into a logical analysis by synthesizing a system of weighted constraints, and a back-end, which is a learning and inference engine for such constraints. I will demonstrate how this approach advances three important applications of program analysis: automated verification, interactive verification, and bug detection. I will also describe new algorithmic techniques to solve very large instances of weighted constraints that arise not only in our domain but also in other domains such as Big Data analytics and statistical AI.
Mayur Naik is an Associate Professor of Computer Science at the University of Pennsylvania. His research spans all aspects of programming systems with the goal of improving software quality and programmer productivity. His current work seeks to develop advanced programming systems that effectively combine the power of humans, computers, and data. He holds a Ph.D. in Computer Science from Stanford University (2008). He was a researcher at Intel Labs, Berkeley from 2008 to 2011, and on the faculty at Georgia Tech from 2011 to 2016.