Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our Airac Experience∗

We present our experience of combining, in a realistic setting, a static analysis for soundness and a statistical analysis for false-alarm removal. The static analyzer is Airac that we have developed in the abstract interpretation framework for detecting buffer over-runs in ANSI + GNU C programs. Airac is sound (finding all bugs) but with false alarms. Airac raised, for example, 970 buffer-overrun alarms in commercial C programs of 5.3 million lines and 233 among the 970 alarms were true. We addressed the false alarm problem by computing a probability of each alarm being true. We used Bayesian analysis and Monte Carlo method to estimate the probabilities and their credible sets. Depending on the user-provided ratio of the risk of silencing true alarms to that of false alarming, the system selectively present the analysis results (alarms) to the user. Though preliminary, the performance of the combination let us not hastefully trade the analysis soundness for a reduced number of false alarms.