Abstract

Program analysis tools require annotations in order to be effective. We present techniques to guess annotations using hints from the programmer. In our experience, we find that it is easier for programmers to give hints, if we allow specifying facts that are likely to hold. For instance, the programmer might state that if a pointer is probed inside a method and then accessed, then it is very likely that the pointer has not been validated on entry to the method. We propose using probabilistic inference to deal with such hints, using probability as the uniform currency in representing and manipulating uncertainty. We give two examples from our experience: (1) Merlin, an inference engine for information flow annotations, and (2) Anek, an inference engine for aliasing annotations known as access permissions. These experiences have led to a general framework called BayeZ for guessing annotations via a combination of logical and probabilistic inference. We present preliminary results for BayeZ together with applications beyond programming languages.