Combining logical and probabilistic reasoning in program analysis

Abstract

Software is becoming increasingly pervasive and complex. These trends expose masses of users to unintended software failures and deliberate cyber-attacks. A widely adopted solution to enforce software quality is automated program analysis. Existing program analyses are expressed in the form of logical rules that are handcrafted by experts. While such a logic-based approach provides many benefits, 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. We seek to address these limitations by proposing a methodology and framework for incorporating probabilistic reasoning directly into existing program analyses that are based on logical reasoning. The framework consists of a frontend, which automatically integrates probabilities into a logical analysis by synthesizing a system of weighted constraints, and a backend, which is a learning and inference engine for such constraints. We demonstrate that the combined approach can benefit a number of important applications of program analysis and thereby facilitate more widespread adoption of this technology. We 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.