MIP-1205

Paper Description

BibTeX entry

@incollection{MIP-1205,
author={D. Beyer, S. Löwe},
title={{Explicit-Value Analysis Based on CEGAR and Interpolation}},
institution={{Fakult{\"a}t f{\"u}r Informatik und Mathematik, Universit{\"a}t Passau}},
year={2012},
number={MIP-1205}
}

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.

Paper itself

MIP-1205.pdf