Abstract: Logical abduction is an inference technique that aims to infer missing hypotheses, and our recent work has shown that abductive reasoning is useful for improving the precision, scalability, and usability of static program analysis. In this talk, we present an abduction-based approach that overcomes a fundamental weakness in the usability of existing static analyzers by helping programmers diagnose the root cause of warnings. Specifically, we present an “introspective” static analysis that can reason about its own shortcomings in order to help programmers diagnose whether a warning corresponds to a real bug or false alarm. Our technique is interactive and integrates programmer feedback by asking the user a series of relevant yes/no queries. We show how query generation can be formulated in terms of logical abduction, and we present a new algorithm for performing abduction in logical theories that are commonly used in program verification. We have evaluated this approach by performing a user study and demonstrate that our technique dramatically improves the usability of static analysis for programmers.
Bio: Isil Dillig is an Assistant Professor of Computer Science at the University of Texas at Austin where she leads the UToPiA research group. Her main research area is programming languages, with a specific emphasis on static analysis, verification, and program synthesis. The techniquesdeveloped by her group aim to make software systems more reliable, secure, and easier to build in a robust way. Dr. Dillig is a Sloan Fellow and a recipient of the NSF CAREER award. She obtained all her degrees (BS, MS, and PhD) from Stanford University. Prior to joining UT Austin, Dr. Dillig worked as a researcher at Microsoft Research and as an assistant professor of computer science at the College of William & Mary. Outside of work, she enjoys hiking, scuba diving, and photography.