Explicit-Value Analysis Based on CEGAR and Interpolation
Abstract
Abstraction, counterexample-guided refinement, and interpolation are techniques that are essential to the success of predicate-based program analysis. These techniques have not yet been applied together to explicit-value program analysis. We present an approach that integrates abstraction and interpolation-based refinement into an explicit-value analysis, i.e., a program analysis that tracks explicit 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 evaluate 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. In addition, we show that combining our new approach with an auxiliary predicate analysis scores significantly higher than the SV-COMP'12 winner.
Keywords
Cite
@article{arxiv.1212.6542,
title = {Explicit-Value Analysis Based on CEGAR and Interpolation},
author = {Dirk Beyer and Stefan Löwe},
journal= {arXiv preprint arXiv:1212.6542},
year = {2013}
}
Comments
12 pages, 5 figures, 3 tables, 4 algorithms