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

23 Citations (Scopus)


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
Number of pages16
ISBN (Electronic)978-3-642-34281-3
ISBN (Print)978-3-642-34280-6
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
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference14th International Conference on Formal Engineering Methods, ICFEM 2012
Abbreviated titleICFEM


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


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

Cite this