A method for scalable and precise bug finding using program analysis and model checking

Abstract

We have applied our analysis to detect memory leaks and implemented it using aspects of the Parfait static code analysis tool and the SPIN model checker. Results show that our approach scales to large code bases and has good precision: the analysis runs over 1 million lines of noncommented C++ OpenJDKTM source code in 1 hour and 19 minutes, with a precision of 84.5%. Further, our analysis found 62.2% more defects when compared to the dataflow approach used by Oracle Parfait’s memory leak checker. This paper presents a technique for defect detection in large code bases called model-based analysis. It incorporates ideas and techniques from program analysis and model checking. Model checking, while very precise, is unable to handle large code bases that are in the millions of lines of code. Thus we create a number of abstract programs from the large code base which can all be model checked. In order to create these abstract programs, we first identify potential defects quickly via static analysis. Second we create a program slice containing one potential defect. Each slice is then abstracted using a combination of automatic data and predicate abstraction. This abstracted model is then model checked to verify the existence or absence of the defect. By applying model checking to a large number of small models instead of one single large model makes our approach scalable without compromising on precision.