Structural Abstraction of Software Verification Conditions
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{bh07structural,
author = {Domagoj Babi\'c and Alan J. Hu},
title = {{Structural Abstraction of Software Verification Conditions}},
booktitle = {CAV'07: Proceedings of the 19th International
Conference on Computer Aided Verification},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
location = {Berlin, Germany},
month = {July},
year = {2007},
volume = {4590},
pages = {371--383}
}
Abstract:
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.