Interpolation for Value Analysis
Dirk Beyer, Stefan Löwe · Software Engineering & Management · 2015
Abstraction, counterexample-guided refinement, and interpolation are tech- niques that are essential to the success of predicate-based program analysis. These techniques have not yet been applied together to value analysis. We present an approach that integrates abstraction and interpolation-based refinement into a value analysis, i.e., a program analysis that tracks values for a specified set of variables (the precision). The algorithm uses an abstract reachability graph as central data structure and a path- sensitive dynamic approach for precision adjustment. We evaluated our algorithm on the benchmark set of the Competition on Software Verification 2012 (SV-COMP'12) to show that our new approach is highly competitive. We also showed that combining our new approach with an auxiliary predicate analysis scores significantly higher than the SV-COMP'12 winner.