Skip to main content

Introspective Static Analysis via Abductive Inference

Isil Dillig ( University of Texas, Austin )

When software veriļ¬cation tools fail to prove the correctness a program, there are two possibilities: Either the program is indeed buggy  or the warning generated by the analysis is a false alarm. In this situation, the burden is on the programmer to manually inspect the warning and decide whether the program contains a real bug. However, this task is quite error-prone and time consuming and remains an impediment to the adoption of static analysis in the real world. In this talk, we present a new "introspective" approach to static analysis that helps programmers understand and diagnose error reports generated by the analysis. When our analysis fails to verify the program, it can meaningfully interact with users by generating small and relevant queries that capture exactly the information the analysis is missing to validate or refute the existence of an error in the program. The inference of such missing facts is an instance of logical abduction, and we present a new algorithm for performing abductive inference in logics that admit quantifier elimination. Since our abduction algorithm computes logically weakest solutions with as few variables as possible, the queries our technique presents to the user capture the minimum information needed to diagnose the error report. A user study we performed involving 56 programmers hired through ODesk indicates that our new technique dramatically improves the usefulness of static analysis to programmers.

Speaker bio

Isil Dillig is an assistant professor of computer science at the University of Texas at Austin. She received all her degrees (BS, MS, PhD) in computer science from Stanford University. Prior to joining Austin, she worked as a researcher at Microsoft Research in Cambridge UK (2013-2014) and as an assistant professor at the College of William & Mary in Virginia (2012-2013). Isil's research interests include program analysis and verification, programming languages, formal methods, and automated logical reasoning.

Share this: