B. Mihaila, A. Sepp and A. Simon. Widening as Abstract Domain. In G. Brat, N. Rungta and A. Venet, editors, NASA Formal Methods, volume 7871 of LNCS, pages 170--186, Moffett Field, California, USA, May 2013. Springer.

Verification using static analysis often hinges on precise numeric invariants. Numeric domains of infinite height can infer these invariants, but require widening/narrowing which complicates the fixpoint computation and is often too imprecise. As a consequence, several strategies have been proposed to prevent a precision loss during widening or to narrow in a smarter way. Most of these strategies are difficult to retrofit into an existing analysis as they either require a pre-analysis, an on-the-fly modification of the CFG, or modifications to the fixpoint algorithm. We propose to encode widening and its various refinements from the literature as co-fibered abstract domains that wrap standard numeric domains, thereby providing a way to add numeric analysis to any static analysis, that is, without modifying the fixpoint engine. Since these domains cannot make any assumptions about the structure of the program, our approach is suitable to the analysis of executables, where the (potentially irreducible) CFG is re-constructed on-the-fly. Moreover, our domain-based approach not only mirrors the precision of more intrusive approaches in the literature but also requires fewer iterations to find a fixpoint of loops than many heuristics that merely aim for precision.

Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com