Counterexample Guided Path Reduction for Static Program Analysis

Abstract. In this work we introduce counterexample guided path reduction based on interval constraint solving for static program analysis. The aim of this technique is to reduce the number of false positives by rehe number of feasible paths in the abstraction iteratively. Given a counterexample, a set of observers is computed which exclude infeasible paths in the next iteration. This approach combines ideas from xample guided abstraction refinement for software verification with static analysis techniques that employ interval constraint solving. The advantage is that the analysis becomes less conservative than static analysis, while it benefits from the fact that interval constraint solving deals naturally with loops. We demonstrate that the proposed approach is effective in reducing the number of false positives, and compare it to other static checkers for C/C++ program analysis.

• Type: Conference
• Year: 2010
• Where: BIRTHDAY
• Authors: Ansgar Fehnker, Ralf Huuck, Sean Seefried
• Keywords: Applied Computing, BIRTHDAY 2010, Constraint Solving, Interval Constraint, Static Analysis