Title
Comparing model checking and static program analysis: A case study in error detection approaches
Date of this Version
10-6-2010
Document Type
Conference Paper
Abstract
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 is currently not available here.
This document has been peer reviewed.
Publication Details
Interim status: Citation only.
Vorobyov, K. & Krishnan, P. (2010). Comparing model checking and static program analysis: A case study in error detection approaches. Paper presented at the 5th international workshop on Systems Software Verification (SSV '10), Vancouver, Canada.
Access the conference website.
2010 HERDC submission. FoR Code: 080600
© Copyright Kostyantyn Vorobyov and Padmanabhan Krishnan, 2010