Colloquium Details
Precise Program Reasoning using Probabilistic Methods
Speaker: Mukund Raghothaman, University of Pennsylvania
Location: 60 Fifth Avenue 150
Date: February 11, 2019, 2 p.m.
Host: Subhash Khot
Synopsis:
The enormous rise in the scale, scope, and complexity of software projects has created a thriving marketplace for program analysis and verification tools. Despite routine adoption by industry, developing such tools remains challenging, and their designers must carefully balance tradeoffs between false alarms, missed bugs, and scalability to large codebases. Furthermore, when tools fail to verify some program property, they only provide coarse estimates of alarm relevance, potential severity, and of the likelihood of being a real bug, thereby limiting their usefulness in software projects with large teams.
I will present a framework that extends contemporary program reasoning systems with rich probabilistic models. These models emerge naturally from the program structure, and probabilistic inference refines the deductive process of the underlying system. In experiments with large programs, such probabilistic graphical representations of program structure enable an order-of-magnitude reduction in false alarm rates and invocations of expensive reasoning engines such as SMT solvers.
To the analysis user, these techniques offer a lens by which to focus their attention on the most important alarms and a uniform method for the tool to interactively generalize from human feedback. To the analysis designer, they offer novel opportunities to leverage data-driven approaches in analysis design. And to researchers, they offer new challenges while performing inference in models of unprecedented size. I will conclude by describing how these ideas promise to underpin the next generation of intelligent programming systems, with applications in diverse areas such as program synthesis, differentiable programming, and fault localization in complex systems.
Speaker Bio:
Mukund Raghothaman is a postdoctoral researcher at the University of Pennsylvania. His research spans the areas of programming languages, software verification, and program synthesis, with the ultimate goal to help programmers create better software with less effort. He previously obtained a Ph.D. in 2017, also from the University of Pennsylvania, where he developed programming abstractions for data stream processing systems.
Notes:
In-person attendance only available to those with active NYU ID cards.