Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our Airac Experience ⁄
Yungbum Jung, JaeHwang Kim, Jaeho Shin, Kwangkeun Yi · 2005
We present our experience of combining, in a realistic set-ting, 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 bu®er overruns in ANSI + GNU C programs. Airac is sound (¯nding all bugs) but with false alarms. Airac raised, for example, 1009 bu®er-overrun alarms in commer-cial C programs of 636K lines and 183 among the 1009 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 lets us not hastily trade the analysis soundness for a reduced number of false alarms. 1.