Incremental False Path Elimination for Static Software Analysis

Ansgar Fehnker; Ralf Huuck; Sean Seefried

doi:10.1007/978-3-642-04761-9_20

Incremental False Path Elimination for Static Software Analysis

Ansgar Fehnker, Ralf Huuck, Sean Seefried

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

Abstract

In this work we introduce a novel approach for removing false positives in static program analysis. We present an incremental algorithm that investigates paths to failure locations with respect to feasibility. The feasibility test it done by interval constraint solving over a semantic abstraction of program paths. Sets of infeasible paths can be ruled out by enriching the analysis incrementally with observers. Much like counterexample guided abstraction refinement for software verification our approach enables to start static program analysis with a coarse syntactic abstraction and use richer semantic information to rule out false positives when necessary and possible. Moreover, we present our implementation in the Goanna static analyzer and compare it to other tools for C/C++ program analysis.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings
Editors	Zhiming Liu, Anders P. Ravn
Publisher	Springer
Pages	255-270
Number of pages	16
ISBN (Electronic)	978-3-642-04761-9
ISBN (Print)	978-3-642-04760-2
DOIs	https://doi.org/10.1007/978-3-642-04761-9_20
Publication status	Published - 2009
Externally published	Yes
Event	7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009 - Macao, China Duration: 14 Oct 2009 → 16 Oct 2009 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	5799

Conference

Conference	7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009
Abbreviated title	ATVA
Country/Territory	China
City	Macao
Period	14/10/09 → 16/10/09

Access to Document

10.1007/978-3-642-04761-9_20

Cite this

Fehnker, A., Huuck, R., & Seefried, S. (2009). Incremental False Path Elimination for Static Software Analysis. In Z. Liu, & A. P. Ravn (Eds.), Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings (pp. 255-270). (Lecture Notes in Computer Science; Vol. 5799). Springer. https://doi.org/10.1007/978-3-642-04761-9_20

@inproceedings{e2ac395ab61d418f871731088225632c,

title = "Incremental False Path Elimination for Static Software Analysis",

abstract = "In this work we introduce a novel approach for removing false positives in static program analysis. We present an incremental algorithm that investigates paths to failure locations with respect to feasibility. The feasibility test it done by interval constraint solving over a semantic abstraction of program paths. Sets of infeasible paths can be ruled out by enriching the analysis incrementally with observers. Much like counterexample guided abstraction refinement for software verification our approach enables to start static program analysis with a coarse syntactic abstraction and use richer semantic information to rule out false positives when necessary and possible. Moreover, we present our implementation in the Goanna static analyzer and compare it to other tools for C/C++ program analysis.",

author = "Ansgar Fehnker and Ralf Huuck and Sean Seefried",

year = "2009",

doi = "10.1007/978-3-642-04761-9_20",

language = "English",

isbn = "978-3-642-04760-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "255--270",

editor = "Zhiming Liu and Ravn, {Anders P.}",

booktitle = "Automated Technology for Verification and Analysis",

address = "Germany",

note = "7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, ATVA ; Conference date: 14-10-2009 Through 16-10-2009",

}

Fehnker, A, Huuck, R & Seefried, S 2009, Incremental False Path Elimination for Static Software Analysis. in Z Liu & AP Ravn (eds), Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5799, Springer, pp. 255-270, 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, Macao, China, 14/10/09. https://doi.org/10.1007/978-3-642-04761-9_20

Incremental False Path Elimination for Static Software Analysis. / Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean.
Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. ed. / Zhiming Liu; Anders P. Ravn. Springer, 2009. p. 255-270 (Lecture Notes in Computer Science; Vol. 5799).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Incremental False Path Elimination for Static Software Analysis

AU - Fehnker, Ansgar

AU - Huuck, Ralf

AU - Seefried, Sean

N1 - Conference code: 7

PY - 2009

Y1 - 2009

N2 - In this work we introduce a novel approach for removing false positives in static program analysis. We present an incremental algorithm that investigates paths to failure locations with respect to feasibility. The feasibility test it done by interval constraint solving over a semantic abstraction of program paths. Sets of infeasible paths can be ruled out by enriching the analysis incrementally with observers. Much like counterexample guided abstraction refinement for software verification our approach enables to start static program analysis with a coarse syntactic abstraction and use richer semantic information to rule out false positives when necessary and possible. Moreover, we present our implementation in the Goanna static analyzer and compare it to other tools for C/C++ program analysis.

AB - In this work we introduce a novel approach for removing false positives in static program analysis. We present an incremental algorithm that investigates paths to failure locations with respect to feasibility. The feasibility test it done by interval constraint solving over a semantic abstraction of program paths. Sets of infeasible paths can be ruled out by enriching the analysis incrementally with observers. Much like counterexample guided abstraction refinement for software verification our approach enables to start static program analysis with a coarse syntactic abstraction and use richer semantic information to rule out false positives when necessary and possible. Moreover, we present our implementation in the Goanna static analyzer and compare it to other tools for C/C++ program analysis.

U2 - 10.1007/978-3-642-04761-9_20

DO - 10.1007/978-3-642-04761-9_20

M3 - Conference contribution

SN - 978-3-642-04760-2

T3 - Lecture Notes in Computer Science

SP - 255

EP - 270

BT - Automated Technology for Verification and Analysis

A2 - Liu, Zhiming

A2 - Ravn, Anders P.

PB - Springer

T2 - 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009

Y2 - 14 October 2009 through 16 October 2009

ER -

Incremental False Path Elimination for Static Software Analysis

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this