Structural Abstraction of Software Verification Conditions

Domagoj Babic, and Alan J. Hu

Computer-Aided Verification:  19th International Conference (CAV 2007)

Precise software analysis and verification require tracking the exact
path along which a statement is executed (path-sensitivity), the
different contexts from which a function is called
(context-sensitivity), and the bit-accurate operations performed.
Previously, verification with such precision has been considered too
inefficient to scale to large software.  In this paper, we present a
novel approach to solving such verification conditions, based on an
automatic abstraction-checking-refinement framework that exploits
natural abstraction boundaries present in software.  Experimental
results show that our approach easily scales to over 200,000 lines of
real C/C++ code.