Incremental false path elimination for static software analysis 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.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Brauer, Jörg; King, Andy; Kowalewski, Stefan: Abstract interpretation of microcontroller code: intervals meet congruences (2013)
- Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Counterexample guided path reduction for static program analysis (2010)
- Peleska, Jan: Integrated and automated abstract interpretation, verification and testing of C/C++ modules (2010)
- Brauer, Jörg; Huuck, Ralf; Schlich, Bastian: Interprocedural pointer analysis in goanna (2009)
- Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Incremental false path elimination for static software analysis (2009)
- Hashimoto, Yuusuke; Nakajima, Shin: Modular checking with model checking (2009)
- Vistein, Michael; Ortmeier, Frank; Reif, Wolfgang; Huuck, Ralf; Fehnker, Ansgar: An abstract specification language for static program analysis (2009)
- Löding, Helge; Peleska, Jan: Symbolic and abstract interpretation for C/C++ programs. (2008)