SMT-Based False Positive Elimination in Static Program Analysis

Maximilian Junker, Ralf Huuck, Ansgar Fehnker, Alexander Knapp

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

21 Citations (Scopus)

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 to 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.
Original languageEnglish
Title of host publicationFormal Methods and Software Engineering
Subtitle of host publication14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings
EditorsToshiaki Aoki, Kenji Taguchi
Place of PublicationBerlin
PublisherSpringer
Pages316-331
Number of pages16
ISBN (Electronic)978-3-642-34281-3
ISBN (Print)978-3-642-34280-6
DOIs
Publication statusPublished - 2012
Externally publishedYes
Event14th International Conference on Formal Engineering Methods, ICFEM 2012 - Kyoto, Japan
Duration: 12 Nov 201216 Nov 2012
Conference number: 14

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume7635
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Conference on Formal Engineering Methods, ICFEM 2012
Abbreviated titleICFEM
CountryJapan
CityKyoto
Period12/11/1216/11/12

Keywords

  • Model Check
  • Bound Model Check
  • Model Check Problem
  • Static Analysis Tool
  • Static Program Analysis

Fingerprint Dive into the research topics of 'SMT-Based False Positive Elimination in Static Program Analysis'. Together they form a unique fingerprint.

  • Cite this

    Junker, M., Huuck, R., Fehnker, A., & Knapp, A. (2012). SMT-Based False Positive Elimination in Static Program Analysis. In T. Aoki, & K. Taguchi (Eds.), Formal Methods and Software Engineering: 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings (pp. 316-331). (Lecture Notes in Computer Science; Vol. 7635). Berlin: Springer. https://doi.org/10.1007/978-3-642-34281-3_23