Comparing model checking and static program analysis: A case study in error detection approaches
Date of this Version
Static program analysis and model checking are two different techniques in bug detection that perform error checking statically, without running the program. In general, static program analysis determines run-time properties of programs by examining the code structure while model checking needs to explore the relevant states of the computation.
This paper reports on a comparison of such approaches via an empirical evaluation of tools that implement these techniques: CBMC - a bounded model checker and Parfait - a static program analysis tool. These tools are run over code repositories with known, marked in the code bugs. We indicate the performance of these tools and report on statistics of found and missed bugs. Our results illustrate the relative strengths of each approach.
This document has been peer reviewed.