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

Fingerprint

Surface mount technology
Model checking
Static analysis
Experiments

Keywords

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

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
Junker, Maximilian ; Huuck, Ralf ; Fehnker, Ansgar ; Knapp, Alexander. / SMT-Based False Positive Elimination in Static Program Analysis. Formal Methods and Software Engineering: 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings. editor / Toshiaki Aoki ; Kenji Taguchi. Berlin : Springer, 2012. pp. 316-331 (Lecture Notes in Computer Science).
@inproceedings{b59ab7dbaf614025a7f744d6fc31ee64,
title = "SMT-Based False Positive Elimination in Static Program Analysis",
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.",
keywords = "Model Check, Bound Model Check, Model Check Problem, Static Analysis Tool, Static Program Analysis",
author = "Maximilian Junker and Ralf Huuck and Ansgar Fehnker and Alexander Knapp",
year = "2012",
doi = "10.1007/978-3-642-34281-3_23",
language = "English",
isbn = "978-3-642-34280-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "316--331",
editor = "Toshiaki Aoki and Kenji Taguchi",
booktitle = "Formal Methods and Software Engineering",

}

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. Lecture Notes in Computer Science, vol. 7635, Springer, Berlin, pp. 316-331, 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, 12/11/12. https://doi.org/10.1007/978-3-642-34281-3_23

SMT-Based False Positive Elimination in Static Program Analysis. / Junker, Maximilian; Huuck, Ralf; Fehnker, Ansgar ; Knapp, Alexander.

Formal Methods and Software Engineering: 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings. ed. / Toshiaki Aoki; Kenji Taguchi. Berlin : Springer, 2012. p. 316-331 (Lecture Notes in Computer Science; Vol. 7635).

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

TY - GEN

T1 - SMT-Based False Positive Elimination in Static Program Analysis

AU - Junker, Maximilian

AU - Huuck, Ralf

AU - Fehnker, Ansgar

AU - Knapp, Alexander

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

KW - Model Check

KW - Bound Model Check

KW - Model Check Problem

KW - Static Analysis Tool

KW - Static Program Analysis

U2 - 10.1007/978-3-642-34281-3_23

DO - 10.1007/978-3-642-34281-3_23

M3 - Conference contribution

SN - 978-3-642-34280-6

T3 - Lecture Notes in Computer Science

SP - 316

EP - 331

BT - Formal Methods and Software Engineering

A2 - Aoki, Toshiaki

A2 - Taguchi, Kenji

PB - Springer

CY - Berlin

ER -

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