Structural Abstraction of Software Verification Conditions

[PDF] [PS] [PS.BZ2]

@inproceedings{bh07structural,
  author = {Domagoj Babi\'c and Alan J. Hu},
  title = {{Structural Abstraction of Software Verification Conditions}},
  booktitle = {Computer Aided Verification, 19th International 
    Conference, CAV 2007, Berlin, Germany, July 3--7, 2007, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  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.