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

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

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.

Share

COinS
 

This document has been peer reviewed.