Junker, M. and Huuck, R. and Fehnker, Ansgar and Knapp, A. (2012) SMT - based false positive elimination in static program analysis. [Conference Proceedings]
Preview |
PDF
- Accepted Version
Download (364kB) | Preview |
Abstract
Static program analysis for bug detection in large C/C++ projects typically uses a high-level abstraction of the original program under investigation. As a result, so-called false positives are often inevitable, i.e., warnings that are not true bugs. In this work we present a novel abstraction refinement approach to automatically investigate and eliminate such false positives. Central to our approach is to view static analysis as a model checking problem, to iteratively compute infeasible sub-paths of infeasible paths using SMT solvers, and refine our models by adding observer automata to exclude such paths. Based on this new framework we present an implementation of the approach into the static analyzer Goanna and discuss a number of real-life experiments on larger C code projects, demonstrating that we were able to remove most false positives automatically.
| Item Type: | Conference Proceedings |
|---|---|
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| Divisions: | Faculty of Science, Technology and Environment (FSTE) > School of Computing, Information and Mathematical Sciences |
| Depositing User: | Ansgar Fehnker |
| Date Deposited: | 01 May 2013 03:23 |
| Last Modified: | 31 Jul 2016 23:08 |
| URI: | https://repository.usp.ac.fj/id/eprint/5728 |
Actions (login required)
 |
View Item |