Introspective Static Analysis via Abductive Inference

When software verification 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.