Comparing Model Checking and Static Program Analysis: A Case Study

Static program analysis and model checking are two dif-ferent techniques in bug detection that perform error checking statically, without running the program. In gen-eral, static program analysis determines run-time proper-ties 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 Par-fait – 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 re-port on statistics of found and missed bugs. Our results illustrate the relative strengths of each approach.